1  /-
  2  Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Sébastien Gouëzel
  5  -/
  6  
  7  import topology.topological_fiber_bundle geometry.manifold.smooth_manifold_with_corners
src         └───────────────────────────────┘ └────────────────────────────────────────────┘
  8  /-!
  9  # Basic smooth bundles
 10  
 11  In general, a smooth bundle is a bundle over a smooth manifold, whose fiber is a manifold, and
 12  for which the coordinate changes are smooth. In this definition, there are charts involved at
 13  several places: in the manifold structure of the base, in the manifold structure of the fibers, and
 14  in the local trivializations. This makes it a complicated object in general. There is however a
 15  specific situation where things are much simpler: when the fiber is a vector space (no need for
 16  charts for the fibers), and when the local trivializations of the bundle and the charts of the base
 17  coincide. Then everything is expressed in terms of the charts of the base, making for a much
 18  simpler overall structure, which is easier to manipulate formally.
 19  
 20  Most vector bundles that naturally occur in differential geometry are of this form:
 21  the tangent bundle, the cotangent bundle, differential forms (used to define de Rham cohomology)
 22  and the bundle of Riemannian metrics. Therefore, it is worth defining a specific constructor for
 23  this kind of bundle, that we call basic smooth bundles.
 24  
 25  A basic smooth bundle is thus a smooth bundle over a smooth manifold whose fiber is a vector space,
 26  and which is trivial in the coordinate charts of the base. (We recall that in our notion of manifold
 27  there is a distinguished atlas, which does not need to be maximal: we require the triviality above
 28  this specific atlas). It can be constructed from a basic smooth bundled core, defined below,
 29  specifying the changes in the fiber when one goes from one coordinate chart to another one. We do
 30  not require that this changes in fiber are linear, but only diffeomorphisms.
 31  
 32  ## Main definitions
 33  
 34  * `basic_smooth_bundle_core I M F`: assuming that `M` is a smooth manifold over the model with
 35    corners `I` on `(𝕜, E, H)`, and `F` is a normed vector space over `𝕜`, this structure registers,
 36    for each pair of charts of `M`, a smooth change of coordinates on `F`. This is the core structure
 37    from which one will build a smooth bundle with fiber `F` over `M`.
 38  
 39  Let `Z` be a basic smooth bundle core over `M` with fiber `F`. We define
 40  `Z.to_topological_fiber_bundle_core`, the (topological) fiber bundle core associated to `Z`. From it,
 41  we get a space `Z.to_topological_fiber_bundle_core.total_space` (which as a Type is just `M × F`),
 42  with the fiber bundle topology. It inherits a manifold structure (where the charts are in bijection
 43  with the charts of the basis). We show that this manifold is smooth.
 44  
 45  Then we use this machinery to construct the tangent bundle of a smooth manifold.
 46  
 47  * `tangent_bundle_core I M`: the basic smooth bundle core associated to a smooth manifold `M` over a
 48    model with corners `I`.
 49  * `tangent_bundle I M`     : the total space of `tangent_bundle_core I M`. It is itself a
 50    smooth manifold over the model with corners `I.tangent`, the product of `I` and the trivial model
 51    with corners on `E`.
 52  * `tangent_space I x`      : the tangent space to `M` at `x`
 53  * `tangent_bundle.proj I M`: the projection from the tangent bundle to the base manifold
 54  
 55  ## Implementation notes
 56  
 57  In the definition of a basic smooth bundle core, we do not require that the coordinate changes of
 58  the fibers are linear map, only that they are diffeomorphisms. Therefore, the fibers of the
 59  resulting fiber bundle do not inherit a vector space structure (as an algebraic object) in general.
 60  As the fiber, as a type, is just `F`, one can still always register the vector space structure, but
 61  it does not make sense to do so (i.e., it will not lead to any useful theorem) unless this structure
 62  is canonical, i.e., the coordinate changes are linear maps.
 63  
 64  For instance, we register the vector space structure on the fibers of the tangent bundle. However,
 65  we do not register the normed space structure coming from that of `F` (as it is not canonical, and
 66  we also want to keep the possibility to add a Riemannian structure on the manifold later on without
 67  having two competing normed space instances on the tangent spaces).
 68  
 69  We require `F` to be a normed space, and not just a topological vector space, as we want to talk
 70  about smooth functions on `F`. The notion of derivative requires a norm to be defined.
 71  
 72  ## TODO
 73  construct the cotangent bundle, and the bundles of differential forms. They should follow
 74  functorially from the description of the tangent bundle as a basic smooth bundle.
 75  
 76  ## Tags
 77  Smooth fiber bundle, vector bundle, tangent space, tangent bundle
 78  -/
 79  
 80  noncomputable theory
 81  
 82  universe u
 83  
 84  open topological_space set
 85  
 86  /-- Core structure used to create a smooth bundle above `M` (a manifold over the model with
 87  corner `I`) with fiber the normed vector space `F` over `𝕜`, which is trivial in the chart domains
 88  of `M`. This structure registers the changes in the fibers when one changes coordinate charts in the
 89  base. We do not require the change of coordinates of the fibers to be linear, only smooth.
 90  Therefore, the fibers of the resulting bundle will not inherit a canonical vector space structure
 91  in general. -/
 92  structure basic_smooth_bundle_core {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
id                                           └───┘   └──────────────────────┘ 
src                                                  └──────────────────────┘
typ                                          └───┘   └──────────────────────┘ 
doc                                                  └──────────────────────┘
 93  {E : Type u} [normed_group E] [normed_space 𝕜 E]
id        └──┘     └──────────┘    └──────────┘  
src                └──────────┘     └──────────┘
typ       └──┘     └──────────┘    └──────────┘  
doc                └──────────┘     └──────────┘
 94  {H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
id        └───┘   └───────────────┘        └────────────────┘   
src               └───────────────┘         └────────────────┘
typ       └───┘   └───────────────┘        └────────────────┘   
doc               └───────────────┘         └────────────────┘
 95  (M : Type*) [topological_space M] [manifold H M] [smooth_manifold_with_corners I M]
id        └───┘   └───────────────┘    └──────┘     └──────────────────────────┘  
src               └───────────────┘     └──────┘       └──────────────────────────┘
typ       └───┘   └───────────────┘    └──────┘     └──────────────────────────┘  
doc               └───────────────┘     └──────┘       └──────────────────────────┘
 96  (F : Type u) [normed_group F] [normed_space 𝕜 F] :=
id        └──┘     └──────────┘    └──────────┘  
src                └──────────┘     └──────────┘
typ       └──┘     └──────────┘    └──────────┘  
doc                └──────────┘     └──────────┘
 97  (coord_change      : atlas H M → atlas H M → H → F → F)
id                        └───┘    └───┘           
src                       └───┘       └───┘
typ                       └───┘    └───┘           
 98  (coord_change_self :
 99    ∀ i : atlas H M, ∀ x ∈ i.1.target, ∀ v, coord_change i i x v = v)
id          └───┘          └────┘       └──────────┘      
src          └───┘             └────┘                             
typ         └───┘          └────┘       └──────────┘      
100  (coord_change_comp : ∀ i j k : atlas H M,
id                                 └───┘  
src                                 └───┘
typ                                └───┘  
101    ∀ x ∈ ((i.1.symm.trans j.1).trans (j.1.symm.trans k.1)).source, ∀ v,
id             └──┘ └───┘    └───┘    └──┘ └───┘     └────┘     
src              └──┘ └───┘     └───┘     └──┘ └───┘      └────┘
typ            └──┘ └───┘    └───┘    └──┘ └───┘     └────┘     
doc               └──┘ └───┘      └───┘      └──┘ └───┘
102    (coord_change j k ((i.1.symm.trans j.1).to_fun x)) (coord_change i j x v) = coord_change i k x v)
id      └──────────┘      └──┘ └───┘    └────┘      └──────────┘       └──────────┘    
src                          └──┘ └───┘     └────┘                             
typ     └──────────┘      └──┘ └───┘    └────┘      └──────────┘       └──────────┘    
doc                           └──┘ └───┘
103  (coord_change_smooth : ∀ i j : atlas H M,
id                                 └───┘  
src                                 └───┘
typ                                └───┘  
104    times_cont_diff_on 𝕜 ⊤ (λp : E × F, coord_change i j (I.inv_fun p.1) p.2)
id     └────────────────┘             └──────────┘    └──────┘    
src    └────────────────┘                                   └──────┘      
typ    └────────────────┘             └──────────┘    └──────┘    
doc    └────────────────┘
105    ((I.to_fun '' (i.1.symm.trans j.1).source).prod (univ : set F)))
id       └─────┘ └┘   └──┘ └───┘    └────┘  └──┘   └──┘   └─┘ 
src       └─────┘ └┘    └──┘ └───┘     └────┘  └──┘   └──┘   └─┘
typ      └─────┘ └┘   └──┘ └───┘    └────┘  └──┘   └──┘   └─┘ 
doc                      └──┘ └───┘              └──┘
106  
107  namespace basic_smooth_bundle_core
108  
109  variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
id                          └──────────────────────┘
src                         └──────────────────────┘
typ                         └──────────────────────┘
doc                         └──────────────────────┘
110  {E : Type u} [normed_group E] [normed_space 𝕜 E]
id                 └──────────┘     └──────────┘
src                └──────────┘     └──────────┘
typ                └──────────┘     └──────────┘
doc                └──────────┘     └──────────┘
111  {H : Type*} [topological_space H] {I : model_with_corners 𝕜 E H}
id                └───────────────┘         └────────────────┘
src               └───────────────┘         └────────────────┘
typ               └───────────────┘         └────────────────┘
doc               └───────────────┘         └────────────────┘
112  {M : Type*} [topological_space M] [manifold H M] [smooth_manifold_with_corners I M]
id                └───────────────┘     └──────┘       └──────────────────────────┘
src               └───────────────┘     └──────┘       └──────────────────────────┘
typ               └───────────────┘     └──────┘       └──────────────────────────┘
doc               └───────────────┘     └──────┘       └──────────────────────────┘
113  {F : Type u} [normed_group F] [normed_space 𝕜 F]
id                 └──────────┘     └──────────┘
src                └──────────┘     └──────────┘
typ                └──────────┘     └──────────┘
doc                └──────────┘     └──────────┘
114  (Z : basic_smooth_bundle_core I M F)
id        └──────────────────────┘
src       └──────────────────────┘
typ       └──────────────────────┘
doc       └──────────────────────┘
115  
116  /-- Fiber bundle core associated to a basic smooth bundle core -/
117  def to_topological_fiber_bundle_core : topological_fiber_bundle_core (atlas H M) M F :=
id                                          └───────────────────────────┘  └───┘     
src                                         └───────────────────────────┘  └───┘
typ                                         └───────────────────────────┘  └───┘     
doc                                         └───────────────────────────┘
118  { base_set := λi, i.1.source,
id                     └────┘
src                      └────┘
typ                    └────┘
119    is_open_base_set := λi, i.1.open_source,
id                             └─────────┘
src                              └─────────┘
typ                            └─────────┘
120    index_at := λx, ⟨chart_at H x, chart_mem_atlas H x⟩,
id                     └──────┘    └─────────────┘  
src                     └──────┘      └─────────────┘
typ                    └──────┘    └─────────────┘  
121    mem_base_set_at := λx, mem_chart_source H x,
id                           └──────────────┘  
src                           └──────────────┘
typ                          └──────────────┘  
122    coord_change := λi j x v, Z.coord_change i j (i.1.to_fun x) v,
id                           └───────────┘     └────┘    
src                               └───────────┘        └────┘
typ                          └───────────┘     └────┘    
123    coord_change_self := λi x hx v, Z.coord_change_self i (i.1.to_fun x) (i.1.map_source hx) v,
id                             └┘   └────────────────┘    └────┘      └────────┘  └┘  
src                                     └────────────────┘      └────┘        └────────┘
typ                            └┘   └────────────────┘    └────┘      └────────┘  └┘  
124    coord_change_comp := λi j k x ⟨⟨hx1, hx2⟩, hx3⟩ v, begin
id                                                
typ                                               
st                                                        └─────
125      have := Z.coord_change_comp i j k (i.1.to_fun x) _ v,
id               └─────────────────┘                    
src      └──────┘└─────────────────┘     └────────┘ └──┘
typ      └──────┘└─────────────────┘  └────────┘└──┘
doc      └──────┘                        └────────┘ └──┘
txt      └──────┘                        └────────┘ └──┘
par      └──────┘                        └────────┘ └──┘
pid      └───┘└─┘                        └────────┘ └──┘
st   ───────────────────────────────────────────────────────┘└─
126      convert this using 2,
id               └──┘
src      └──────┘    └──────┘
typ      └──────┘└──┘└──────┘
doc      └──────┘    └──────┘
txt      └──────┘    └──────┘
par      └──────┘    └──────┘
pid                 └─────┘
st   ───────────────────────┘└─
127      { simp [hx1] },
id               └─┘
src        └────┘   └┘
typ        └────┘└─┘└┘
doc        └────┘   └┘
txt        └────┘   └┘
par        └────┘   └┘
pid               
st   ─────┘└─────────┘└┘
128      { simp [local_equiv.trans_source, hx1, hx2, hx3, i.1.map_source, j.1.map_source] }
id               └──────────────────────┘  └─┘  └─┘  └─┘                 
src        └────┘└──────────────────────┘└┘   └┘   └┘   └┘ └─────────────┘ └─────────────┘
typ        └────┘└──────────────────────┘└┘└─┘└┘└─┘└┘└─┘└┘└─────────────┘└─────────────┘
doc        └────┘                        └┘   └┘   └┘   └┘ └─────────────┘ └─────────────┘
txt        └────┘                        └┘   └┘   └┘   └┘ └─────────────┘ └─────────────┘
par        └────┘                        └┘   └┘   └┘   └┘ └─────────────┘ └─────────────┘
pid                                    └┘   └┘   └┘   └┘ └─────────────┘ └────────────┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
129    end,
st   ────┘
130    coord_change_continuous := λi j, begin
id                                  
typ                                 
st                                      └─────
131      have A : continuous_on (λp : E × F, Z.coord_change i j (I.inv_fun p.1) p.2)
id                └───────────┘            └────────────┘      └───────┘
src      └───────┘└───────────┘  └──┘  └┘└────────────┘   └───────┘ └──┘ └───
typ      └───────┘└───────────┘  └──┘ └┘└────────────┘   └───────┘ └──┘ └───
doc      └───────┘└───────────┘  └──┘   └┘                           └──┘ └───
txt      └───────┘               └──┘   └┘                           └──┘ └───
par      └───────┘               └──┘   └┘                           └──┘ └───
pid      └────┘└─┘               └──┘   └┘                           └──┘ └───
st   ────────────────────────────────────────────────────────────────────────────────
132        ((I.to_fun '' (i.1.symm.trans j.1).source).prod (univ : set F)) :=
id           └──────┘ └┘                                  └──┘   └─┘ 
src  ─────┘  └──────┘└┘  └────────────┘ └───────────────┘ └──┘└─┘└─┘ └─────
typ  ─────┘  └──────┘└┘ └────────────┘└───────────────┘ └──┘└─┘└─┘└─────
doc  ─────┘              └────────────┘ └───────────────┘     └─┘    └─────
txt  ─────┘              └────────────┘ └───────────────┘     └─┘    └─────
par  ─────┘              └────────────┘ └───────────────┘     └─┘    └─────
pid  ─────┘              └────────────┘ └───────────────┘     └─┘    └┘└───
st   ─────────────────────────────────────────────────────────────────────────
133        (Z.coord_change_smooth i j).continuous_on,
id          └───────────────────┘  
src  ─────┘ └───────────────────┘  └─────────────┘
typ  ─────┘ └───────────────────┘└─────────────┘
doc  ─────┘                        └─────────────┘
txt  ─────┘                        └─────────────┘
par  ─────┘                        └─────────────┘
pid  ─────┘                        └────────────┘
st   ──────────────────────────────────────────────┘└─
134      have B : continuous_on (λx : M, I.to_fun (i.1.to_fun x)) i.1.source :=
id                └───────────┘         └──────┘                 
src      └───────┘└───────────┘  └──┘ └┘└──────┘  └────────┘ └─┘ └────────────
typ      └───────┘└───────────┘  └──┘└┘└──────┘  └────────┘ └─┘└────────────
doc      └───────┘└───────────┘  └──┘ └┘          └────────┘ └─┘ └────────────
txt      └───────┘               └──┘ └┘          └────────┘ └─┘ └────────────
par      └───────┘               └──┘ └┘          └────────┘ └─┘ └────────────
pid      └────┘└─┘               └──┘ └┘          └────────┘ └─┘ └──────┘└────
st   ───────────────────────────────────────────────────────────────────────────
135        I.continuous_to_fun.comp_continuous_on i.1.continuous_to_fun,
id         └────────────────────────────────────┘ 
src  ─────┘└────────────────────────────────────┘ └──────────────────┘
typ  ─────┘└────────────────────────────────────┘└──────────────────┘
doc  ─────┘                                       └──────────────────┘
txt  ─────┘                                       └──────────────────┘
par  ─────┘                                       └──────────────────┘
pid  ─────┘                                       └─────────────────┘
st   ─────────────────────────────────────────────────────────────────┘└─
136      have C : continuous_on (λp : M × F, (⟨I.to_fun (i.1.to_fun p.1), p.2⟩ : E × F))
id                └───────────┘              └──────┘                             
src      └───────┘└───────────┘  └──┘   └┘  └──────┘  └────────┘ └───┘ └────┘   └──
typ      └───────┘└───────────┘  └──┘ └┘  └──────┘  └────────┘ └───┘ └────┘ └──
doc      └───────┘└───────────┘  └──┘   └┘            └────────┘ └───┘ └────┘   └──
txt      └───────┘               └──┘   └┘            └────────┘ └───┘ └────┘   └──
par      └───────┘               └──┘   └┘            └────────┘ └───┘ └────┘   └──
pid      └────┘└─┘               └──┘   └┘            └────────┘ └───┘ └────┘   └──
st   ────────────────────────────────────────────────────────────────────────────────────
137               (i.1.source.prod univ),
id                                └──┘
src  ────────────┘  └─────────────┘└──┘
typ  ────────────┘ └─────────────┘└──┘
doc  ────────────┘  └─────────────┘    
txt  ────────────┘  └─────────────┘    
par  ────────────┘  └─────────────┘    
pid  ────────────┘  └─────────────┘    
st   ──────────────────────────────────┘└─
138      { apply continuous_on.prod _ continuous_snd.continuous_on,
id               └────────────────┘   └──────────────────────────┘
src        └────┘└────────────────┘└─┘└──────────────────────────┘
typ        └────┘└────────────────┘└─┘└──────────────────────────┘
doc        └────┘                  └─┘
txt        └────┘                  └─┘
par        └────┘                  └─┘
pid                               └─┘
st   ─────┘└─────────────────────────────────────────────────────┘└─
139        exact B.comp continuous_fst.continuous_on (prod_subset_preimage_fst _ _) },
id               └────┘ └──────────────────────────┘  └──────────────────────┘
src        └────┘└────┘└──────────────────────────┘ └──────────────────────┘└────┘
typ        └────┘└────┘└──────────────────────────┘ └──────────────────────┘└────┘
doc        └────┘                                                           └────┘
txt        └────┘                                                           └────┘
par        └────┘                                                           └────┘
pid                                                                        └───┘
st   ──────────────────────────────────────────────────────────────────────────────┘└┘
140      have C' : continuous_on (λp : M × F, (⟨I.to_fun (i.1.to_fun p.1), p.2⟩ : E × F))
id                 └───────────┘               └──────┘                             
src      └────────┘└───────────┘  └──┘   └┘  └──────┘  └────────┘ └───┘ └────┘   └──
typ      └────────┘└───────────┘  └──┘  └┘  └──────┘  └────────┘ └───┘ └────┘ └──
doc      └────────┘└───────────┘  └──┘   └┘            └────────┘ └───┘ └────┘   └──
txt      └────────┘               └──┘   └┘            └────────┘ └───┘ └────┘   └──
par      └────────┘               └──┘   └┘            └────────┘ └───┘ └────┘   └──
pid      └─────┘└─┘               └──┘   └┘            └────────┘ └───┘ └────┘   └──
st   ─────────────────────────────────────────────────────────────────────────────────────
141                ((i.1.source ∩ j.1.source).prod univ) :=
id                                              └──┘
src  ─────────────┘   └────────┘ └──────────────┘└──┘└────
typ  ─────────────┘  └────────┘└──────────────┘└──┘└────
doc  ─────────────┘   └────────┘  └──────────────┘    └────
txt  ─────────────┘   └────────┘  └──────────────┘    └────
par  ─────────────┘   └────────┘  └──────────────┘    └────
pid  ─────────────┘   └────────┘  └──────────────┘    └───
st   ───────────────────────────────────────────────────────
142        continuous_on.mono C (prod_mono (inter_subset_left _ _) (subset.refl _)),
id         └────────────────┘   └───────┘  └───────────────┘       └─────────┘
src  ─────┘└────────────────┘  └───────┘ └───────────────┘└────┘ └─────────┘└──┘
typ  ─────┘└────────────────┘ └───────┘ └───────────────┘└────┘ └─────────┘└──┘
doc  ─────┘                                               └────┘            └──┘
txt  ─────┘                                               └────┘            └──┘
par  ─────┘                                               └────┘            └──┘
pid  ─────┘                                               └────┘            └──┘
st   ─────────────────────────────────────────────────────────────────────────────┘└─
143      have D : (i.1.source ∩ j.1.source).prod univ ⊆ (λ (p : M × F),
id                                                                
src      └───────┘  └────────┘  └──────────────┘      └────┘   └──
typ      └───────┘  └────────┘  └──────────────┘      └────┘ └──
doc      └───────┘  └────────┘  └──────────────┘       └────┘   └──
txt      └───────┘  └────────┘  └──────────────┘       └────┘   └──
par      └───────┘  └────────┘  └──────────────┘       └────┘   └──
pid      └────┘└─┘  └────────┘  └──────────────┘       └────┘   └──
st   ───────────────────────────────────────────────────────────────────
144        (I.to_fun (i.1.to_fun p.1), p.2)) ⁻¹' ((I.to_fun '' (i.1.symm.trans j.1).source).prod univ),
id                                          └─┘   └──────┘                                    └──┘
src  ─────┘          └────────┘ └───┘ └───┘└─┘  └──────┘    └────────────┘ └───────────────┘└──┘
typ  ─────┘          └────────┘ └───┘ └───┘└─┘  └──────┘   └────────────┘└───────────────┘└──┘
doc  ─────┘           └────────┘ └───┘ └───┘└─┘              └────────────┘ └───────────────┘    
txt  ─────┘           └────────┘ └───┘ └───┘                 └────────────┘ └───────────────┘    
par  ─────┘           └────────┘ └───┘ └───┘                 └────────────┘ └───────────────┘    
pid  ─────┘           └────────┘ └───┘ └───┘                 └────────────┘ └───────────────┘    
st   ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
145      { rintros ⟨x, v⟩ hx,
src        └───────────────┘
typ        └───────────────┘
doc        └───────────────┘
txt        └───────────────┘
par        └───────────────┘
pid               └────────┘
st   ─────┘└───────────────┘└─
146        simp at hx,
src        └────────┘
typ        └────────┘
doc        └────────┘
txt        └────────┘
par        └────────┘
pid            └───┘
st   ───────────────┘└─
147        simp [mem_image_of_mem, local_equiv.trans_source, hx] },
id               └──────────────┘  └──────────────────────┘  └┘
src        └────┘└──────────────┘└┘└──────────────────────┘└┘  └┘
typ        └────┘└──────────────┘└┘└──────────────────────┘└┘└┘└┘
doc        └────┘                └┘                        └┘  └┘
txt        └────┘                └┘                        └┘  └┘
par        └────┘                └┘                        └┘  └┘
pid                            └┘                        └┘  
st   ───────────────────────────────────────────────────────────┘└┘
148      convert continuous_on.comp A C' D,
id               └────────────────┘  └┘ 
src      └──────┘└────────────────┘   
typ      └──────┘└────────────────┘└┘
doc      └──────┘                     
txt      └──────┘                     
par      └──────┘                     
pid                                  
st   ────────────────────────────────────┘└─
149      ext p,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid         └┘
st   ────────┘└─
150      simp
src      └────
typ      └────
doc      └────
txt      └────
par      └────
pid          
st   ─────────
151    end }
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
152  
153  @[simp] lemma base_set (i : atlas H M) :
id                               └───┘  
src                              └───┘
typ                              └───┘  
doc    └──┘
154    Z.to_topological_fiber_bundle_core.base_set i = i.1.source := rfl
id     └───────────────────────────────┘└───────┘    └────┘     └─┘
src     └───────────────────────────────┘└───────┘      └────┘     └─┘
typ    └───────────────────────────────┘└───────┘    └────┘     └─┘
doc     └───────────────────────────────┘
155  
156  /-- Local chart for the total space of a basic smooth bundle -/
157  def chart {e : local_homeomorph M H} (he : e ∈ atlas H M) :
id                  └──────────────┘            └───┘  
src                 └──────────────┘               └───┘
typ                 └──────────────┘            └───┘  
doc                 └──────────────┘
158    local_homeomorph (Z.to_topological_fiber_bundle_core.total_space) (H × F) :=
id     └──────────────┘  └───────────────────────────────┘└──────────┘     
src    └──────────────┘   └───────────────────────────────┘└──────────┘     
typ    └──────────────┘  └───────────────────────────────┘└──────────┘     
doc    └──────────────┘   └───────────────────────────────┘└──────────┘
159  (Z.to_topological_fiber_bundle_core.local_triv ⟨e, he⟩).trans
id    └───────────────────────────────┘└─────────┘    └┘  └───┘
src    └───────────────────────────────┘└─────────┘         └───┘
typ   └───────────────────────────────┘└─────────┘    └┘  └───┘
doc    └───────────────────────────────┘└─────────┘         └───┘
160    (local_homeomorph.prod e (local_homeomorph.refl F))
id      └───────────────────┘   └───────────────────┘ 
src     └───────────────────┘    └───────────────────┘
typ     └───────────────────┘   └───────────────────┘ 
doc     └───────────────────┘    └───────────────────┘
161  
162  @[simp] lemma chart_source (e : local_homeomorph M H) (he : e ∈ atlas H M) :
id                                   └──────────────┘            └───┘  
src                                  └──────────────┘               └───┘
typ                                  └──────────────┘            └───┘  
doc    └──┘                          └──────────────┘
163    (Z.chart he).source = Z.to_topological_fiber_bundle_core.proj ⁻¹' e.source :=
id      └────┘ └┘ └────┘   └───────────────────────────────┘└───┘ └─┘ └─────┘
src      └────┘    └────┘    └───────────────────────────────┘└───┘ └─┘  └─────┘
typ     └────┘ └┘ └────┘   └───────────────────────────────┘└───┘ └─┘ └─────┘
doc      └────┘               └───────────────────────────────┘└───┘ └─┘
164  by { ext p, simp [chart, local_equiv.trans_source] }
id                     └───┘  └──────────────────────┘
src       └───┘  └────┘└───┘└┘└──────────────────────┘└┘
typ       └───┘  └────┘└───┘└┘└──────────────────────┘└┘
doc       └───┘  └────┘└───┘└┘                        └┘
txt       └───┘  └────┘     └┘                        └┘
par       └───┘  └────┘     └┘                        └┘
pid          └┘           └┘                        
st     └──────┘└───────────────────────────────────────┘└┘
165  
166  @[simp] lemma chart_target (e : local_homeomorph M H) (he : e ∈ atlas H M) :
id                                   └──────────────┘            └───┘  
src                                  └──────────────┘               └───┘
typ                                  └──────────────┘            └───┘  
doc    └──┘                          └──────────────┘
167    (Z.chart he).target = e.target.prod univ :=
id      └────┘ └┘ └────┘   └─────┘└───┘ └──┘
src      └────┘    └────┘    └─────┘└───┘ └──┘
typ     └────┘ └┘ └────┘   └─────┘└───┘ └──┘
doc      └────┘                      └───┘
168  begin
st   └─────
169    simp only [chart, local_equiv.trans_target, local_homeomorph.prod_to_local_equiv, id.def,
id                └───┘  └──────────────────────┘  └──────────────────────────────────┘  └────┘
src    └─────────┘└───┘└┘└──────────────────────┘└┘└──────────────────────────────────┘└┘└────┘└─
typ    └─────────┘└───┘└┘└──────────────────────┘└┘└──────────────────────────────────┘└┘└────┘└─
doc    └─────────┘└───┘└┘                        └┘                                    └┘      └─
txt    └─────────┘     └┘                        └┘                                    └┘      └─
par    └─────────┘     └┘                        └┘                                    └┘      └─
pid        └──┘└┘     └┘                        └┘                                    └┘      └─
st   ────────────────────────────────────────────────────────────────────────────────────────────
170          local_equiv.refl_inv_fun, local_homeomorph.trans_to_local_equiv, local_equiv.refl_target,
id           └──────────────────────┘  └───────────────────────────────────┘  └─────────────────────┘
src  ───────┘└──────────────────────┘└┘└───────────────────────────────────┘└┘└─────────────────────┘└─
typ  ───────┘└──────────────────────┘└┘└───────────────────────────────────┘└┘└─────────────────────┘└─
doc  ───────┘                        └┘                                     └┘                       └─
txt  ───────┘                        └┘                                     └┘                       └─
par  ───────┘                        └┘                                     └┘                       └─
pid  ───────┘                        └┘                                     └┘                       └─
st   ──────────────────────────────────────────────────────────────────────────────────────────────────
171          local_homeomorph.refl_local_equiv, local_equiv.prod_target, local_homeomorph.prod_inv_fun],
id           └───────────────────────────────┘  └─────────────────────┘  └───────────────────────────┘
src  ───────┘└───────────────────────────────┘└┘└─────────────────────┘└┘└───────────────────────────┘
typ  ───────┘└───────────────────────────────┘└┘└─────────────────────┘└┘└───────────────────────────┘
doc  ───────┘                                 └┘                       └┘                             
txt  ───────┘                                 └┘                       └┘                             
par  ───────┘                                 └┘                       └┘                             
pid  ───────┘                                 └┘                       └┘                             
st   ─────────────────────────────────────────────────────────────────────────────────────────────────┘└─
172    ext p,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
173    split;
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ─────────
174    simp [e.map_target] {contextual := tt}
id                                        └┘
src    └────┘            └┘ └────────────┘└┘└┘
typ    └────┘└──────────┘└┘ └────────────┘└┘└┘
doc    └────┘            └┘ └────────────┘  └┘
txt    └────┘            └┘ └────────────┘  └┘
par    └────┘            └┘ └────────────┘  └┘
pid                     └────────────┘  
st   ────────────────────────────────────────┘
175  end
st   └─┘
176  
177  /-- The total space of a basic smooth bundle is endowed with a manifold structure, where the charts
178  are in bijection with the charts of the basis. -/
179  instance to_manifold : manifold (H × F) Z.to_topological_fiber_bundle_core.total_space :=
id                          └──────┘      └───────────────────────────────┘└──────────┘
src                         └──────┘         └───────────────────────────────┘└──────────┘
typ                         └──────┘      └───────────────────────────────┘└──────────┘
doc                         └──────┘          └───────────────────────────────┘└──────────┘
180  { atlas := ⋃(e : local_homeomorph M H) (he : e ∈ atlas H M), {Z.chart he},
id                   └──────────────┘            └───┘    └────┘ └┘
src                  └──────────────┘               └───┘       └────┘
typ                  └──────────────┘            └───┘    └────┘ └┘
doc                  └──────────────┘                             └────┘
181    chart_at := λp, Z.chart (chart_mem_atlas H p.1),
id                    └────┘  └─────────────┘  
src                     └────┘  └─────────────┘    
typ                   └────┘  └─────────────┘  
doc                     └────┘
182    mem_chart_source := λp, by simp [mem_chart_source],
id                                     └──────────────┘
src                               └────┘└──────────────┘
typ                              └────┘└──────────────┘
doc                               └────┘                
txt                               └────┘                
par                               └────┘                
pid                                                   
st                               └──────────────────────┘
183    chart_mem_atlas := λp, begin
id                         
typ                        
st                            └─────
184      simp only [mem_Union, mem_singleton_iff, chart_mem_atlas],
id                  └───────┘  └───────────────┘  └─────────────┘
src      └─────────┘└───────┘└┘└───────────────┘└┘└─────────────┘
typ      └─────────┘└───────┘└┘└───────────────┘└┘└─────────────┘
doc      └─────────┘         └┘                 └┘               
txt      └─────────┘         └┘                 └┘               
par      └─────────┘         └┘                 └┘               
pid          └──┘└┘         └┘                 └┘               
st   ────────────────────────────────────────────────────────────┘└─
185      exact ⟨chart_at H p.1, chart_mem_atlas H p.1, rfl⟩
id              └──────┘        └─────────────┘      └─┘
src      └────┘ └──────┘  └──┘└─────────────┘  └──┘└─┘└─
typ      └────┘ └──────┘  └──┘└─────────────┘└──┘└─┘└─
doc      └────┘           └──┘                 └──┘   └─
txt      └────┘           └──┘                 └──┘   └─
par      └────┘           └──┘                 └──┘   └─
pid                      └──┘                 └──┘   
st   ───────────────────────────────────────────────────────
186    end }
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
187  
188  lemma mem_atlas_iff (f : local_homeomorph Z.to_topological_fiber_bundle_core.total_space (H × F)) :
id                            └──────────────┘ └───────────────────────────────┘└──────────┘    
src                           └──────────────┘  └───────────────────────────────┘└──────────┘    
typ                           └──────────────┘ └───────────────────────────────┘└──────────┘    
doc                           └──────────────┘  └───────────────────────────────┘└──────────┘
189    f ∈ atlas (H × F) Z.to_topological_fiber_bundle_core.total_space ↔
id       └───┘      └───────────────────────────────┘└──────────┘ 
src       └───┘         └───────────────────────────────┘└──────────┘ 
typ      └───┘      └───────────────────────────────┘└──────────┘ 
doc                       └───────────────────────────────┘└──────────┘
190    ∃(e : local_homeomorph M H) (he : e ∈ atlas H M), f = Z.chart he :=
id          └──────────────┘            └───┘      └────┘ └┘
src         └──────────────┘               └───┘          └────┘
typ         └──────────────┘            └───┘      └────┘ └┘
doc          └──────────────┘                                 └────┘
191  by simp [atlas, manifold.atlas]
src     └────┘     └┘              └─
typ     └────┘     └┘              └─
doc     └────┘     └┘              └─
txt     └────┘     └┘              └─
par     └────┘     └┘              └─
pid              └┘              
st     └─────────────────────────────
192  
src  
typ  
doc  
txt  
par  
pid  
st   
193  @[simp] lemma mem_chart_source_iff (p q : Z.to_topological_fiber_bundle_core.total_space) :
id                                             └───────────────────────────────┘└──────────┘
src                                             └───────────────────────────────┘└──────────┘
typ                                            └───────────────────────────────┘└──────────┘
doc    └──┘                                     └───────────────────────────────┘└──────────┘
194    p ∈ (chart_at (H × F) q).source ↔ p.1 ∈ (chart_at H q.1).source :=
id        └──────┘       └────┘       └──────┘    └────┘
src        └──────┘          └────┘        └──────┘      └────┘
typ       └──────┘       └────┘       └──────┘    └────┘
195  by simp [chart_at, manifold.chart_at]
src     └────┘        └┘                 └─
typ     └────┘        └┘                 └─
doc     └────┘        └┘                 └─
txt     └────┘        └┘                 └─
par     └────┘        └┘                 └─
pid                 └┘                 
st     └───────────────────────────────────
196  
src  
typ  
doc  
txt  
par  
pid  
st   
197  @[simp] lemma mem_chart_target_iff (p : H × F) (q : Z.to_topological_fiber_bundle_core.total_space) :
id                                                    └───────────────────────────────┘└──────────┘
src                                                      └───────────────────────────────┘└──────────┘
typ                                                   └───────────────────────────────┘└──────────┘
doc    └──┘                                               └───────────────────────────────┘└──────────┘
198    p ∈ (chart_at (H × F) q).target ↔ p.1 ∈ (chart_at H q.1).target :=
id        └──────┘       └────┘       └──────┘    └────┘
src        └──────┘          └────┘        └──────┘      └────┘
typ       └──────┘       └────┘       └──────┘    └────┘
199  by simp [chart_at, manifold.chart_at]
src     └────┘        └┘                 └─
typ     └────┘        └┘                 └─
doc     └────┘        └┘                 └─
txt     └────┘        └┘                 └─
par     └────┘        └┘                 └─
pid                 └┘                 
st     └───────────────────────────────────
200  
src  
typ  
doc  
txt  
par  
pid  
st   
201  @[simp] lemma chart_at_to_fun_fst (p q : Z.to_topological_fiber_bundle_core.total_space) :
id                                            └───────────────────────────────┘└──────────┘
src                                            └───────────────────────────────┘└──────────┘
typ                                           └───────────────────────────────┘└──────────┘
doc    └──┘                                    └───────────────────────────────┘└──────────┘
202    ((chart_at (H × F) q).to_fun p).1 = (chart_at H q.1).to_fun p.1 := rfl
id       └──────┘       └────┘       └──────┘    └────┘       └─┘
src      └──────┘          └────┘        └──────┘      └────┘        └─┘
typ      └──────┘       └────┘       └──────┘    └────┘       └─┘
203  
204  @[simp] lemma chart_at_inv_fun_fst (p : H × F) (q : Z.to_topological_fiber_bundle_core.total_space) :
id                                                    └───────────────────────────────┘└──────────┘
src                                                      └───────────────────────────────┘└──────────┘
typ                                                   └───────────────────────────────┘└──────────┘
doc    └──┘                                               └───────────────────────────────┘└──────────┘
205    ((chart_at (H × F) q).inv_fun p).1 = (chart_at H q.1).inv_fun p.1 := rfl
id       └──────┘       └─────┘       └──────┘    └─────┘       └─┘
src      └──────┘          └─────┘        └──────┘      └─────┘        └─┘
typ      └──────┘       └─────┘       └──────┘    └─────┘       └─┘
206  
207  /-- Smooth manifold structure on the total space of a basic smooth bundle -/
208  instance to_smooth_manifold :
209    smooth_manifold_with_corners (I.prod (model_with_corners_self 𝕜 F))
id     └──────────────────────────┘  └───┘  └─────────────────────┘  
src    └──────────────────────────┘   └───┘  └─────────────────────┘
typ    └──────────────────────────┘  └───┘  └─────────────────────┘  
doc    └──────────────────────────┘   └───┘  └─────────────────────┘
210    Z.to_topological_fiber_bundle_core.total_space :=
id     └───────────────────────────────┘└──────────┘
src     └───────────────────────────────┘└──────────┘
typ    └───────────────────────────────┘└──────────┘
doc     └───────────────────────────────┘└──────────┘
211  begin
st   └─────
212    /- We have to check that the charts belong to the smooth groupoid, i.e., they are smooth on their
st   ────────────────────────────────────────────────────────────────────────────────────────────────────
213    source, and their inverses are smooth on the target. Since both objects are of the same type, it
st   ───────────────────────────────────────────────────────────────────────────────────────────────────
214    suffices to prove the first statement in A below, and then glue back the pieces at the end. -/
st   ─────────────────────────────────────────────────────────────────────────────────────────────────
215    let J := model_with_corners.to_local_equiv (I.prod (model_with_corners_self 𝕜 F)),
id              └───────────────────────────────┘  └────┘  └─────────────────────┘  
src    └───────┘└───────────────────────────────┘ └────┘ └─────────────────────┘  └┘
typ    └───────┘└───────────────────────────────┘ └────┘ └─────────────────────┘└┘
doc    └───────┘                                  └────┘ └─────────────────────┘  └┘
txt    └───────┘                                                                  └┘
par    └───────┘                                                                  └┘
pid    └───┘└─┘                                                                  └┘
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
216    have A : ∀ (e e' : local_homeomorph M H) (he : e ∈ atlas H M) (he' : e' ∈ atlas H M),
id                        └──────────────┘                                      └───┘  
src    └───────┘ └───────┘└──────────────┘  └──────┘        └───────┘   └───┘   
typ    └───────┘ └───────┘└──────────────┘  └──────┘        └───────┘   └───┘ 
doc    └───────┘ └───────┘└──────────────┘  └──────┘         └───────┘           
txt    └───────┘ └───────┘                  └──────┘         └───────┘           
par    └───────┘ └───────┘                  └──────┘         └───────┘           
pid    └────┘└─┘ └───────┘                  └──────┘         └───────┘           
st   ────────────────────────────────────────────────────────────────────────────────────────
217      times_cont_diff_on 𝕜 ⊤
id       └────────────────┘  
src  ───┘└────────────────┘ 
typ  ───┘└────────────────┘
doc  ───┘└────────────────┘  
txt  ───┘                    
par  ───┘                    
pid  ───┘                    
st   ───────────────────────────
218      (J.to_fun ∘ ((Z.chart he).symm.trans (Z.chart he')).to_fun ∘ J.inv_fun)
id                 
src  ───┘                    └───────────┘           └────────┘          └─
typ  ───┘                    └───────────┘           └────────┘          └─
doc  ───┘                     └───────────┘           └────────┘          └─
txt  ───┘                     └───────────┘           └────────┘          └─
par  ───┘                     └───────────┘           └────────┘          └─
pid  ───┘                     └───────────┘           └────────┘          └─
st   ────────────────────────────────────────────────────────────────────────────
219      (J.inv_fun ⁻¹' ((Z.chart he).symm.trans (Z.chart he')).source ∩ range J.to_fun),
id        └───────┘ └─┘                           └─────┘               └───┘ └──────┘
src  ───┘ └───────┘└─┘           └───────────┘ └─────┘   └────────┘└───┘└──────┘
typ  ───┘ └───────┘└─┘           └───────────┘ └─────┘   └────────┘└───┘└──────┘
doc  ───┘          └─┘           └───────────┘ └─────┘   └────────┘ └───┘        
txt  ───┘                        └───────────┘           └────────┘              
par  ───┘                        └───────────┘           └────────┘              
pid  ───┘                        └───────────┘           └────────┘              
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
220    { assume e e' he he',
src      └────────────────┘
typ      └────────────────┘
doc      └────────────────┘
txt      └────────────────┘
par      └────────────────┘
pid      └────────────────┘
st   ───┘└────────────────┘└─
221      have U : unique_diff_on 𝕜
id                └────────────┘ 
src      └───────┘└────────────┘ 
typ      └───────┘└────────────┘
doc      └───────┘└────────────┘ 
txt      └───────┘               
par      └───────┘               
pid      └────┘└─┘               
st   ──────────────────────────────
222               ((I.inv_fun ⁻¹' (e.symm.trans e').source ∩ range I.to_fun).prod (univ : set F)),
id                  └───────┘      └──────────┘ └┘           └───┘ └──────┘        └──┘   └─┘ 
src  ────────────┘  └───────┘    └──────────┘  └───────┘ └───┘└──────┘└─────┘ └──┘└─┘└─┘ └┘
typ  ────────────┘  └───────┘    └──────────┘└┘└───────┘ └───┘└──────┘└─────┘ └──┘└─┘└─┘└┘
doc  ────────────┘               └──────────┘  └───────┘ └───┘        └─────┘     └─┘    └┘
txt  ────────────┘                             └───────┘              └─────┘     └─┘    └┘
par  ────────────┘                             └───────┘              └─────┘     └─┘    └┘
pid  ────────────┘                             └───────┘              └─────┘     └─┘    └┘
st   ───────────────────────────────────────────────────────────────────────────────────────────┘└─
223      { apply unique_diff_on.prod _ unique_diff_on_univ,
id               └─────────────────┘   └─────────────────┘
src        └────┘└─────────────────┘└─┘└─────────────────┘
typ        └────┘└─────────────────┘└─┘└─────────────────┘
doc        └────┘└─────────────────┘└─┘
txt        └────┘                   └─┘
par        └────┘                   └─┘
pid                                └─┘
st   ─────┘└─────────────────────────────────────────────┘└─
224        rw inter_comm,
id            └────────┘
src        └─┘└────────┘
typ        └─┘└────────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ──────────────────┘└─
225        exact I.unique_diff.inter (I.continuous_inv_fun _ (local_homeomorph.open_source _)) },
id               └─────────────────┘  └──────────────────┘    └──────────────────────────┘
src        └────┘└─────────────────┘ └──────────────────┘└─┘ └──────────────────────────┘└───┘
typ        └────┘└─────────────────┘ └──────────────────┘└─┘ └──────────────────────────┘└───┘
doc        └────┘                                        └─┘                             └───┘
txt        └────┘                                        └─┘                             └───┘
par        └────┘                                        └─┘                             └───┘
pid                                                     └─┘                             └──┘
st   ─────────────────────────────────────────────────────────────────────────────────────────┘└┘
226      have : J.inv_fun ⁻¹' ((chart Z he).symm.trans (chart Z he')).source ∩ range J.to_fun =
id              └───────┘               └┘              └───┘  └─┘                  └──────┘ 
src      └─────┘└───────┘             └───────────┘ └───┘    └────────┘      └──────┘
typ      └─────┘└───────┘           └┘└───────────┘ └───┘└─┘└────────┘      └──────┘
doc      └─────┘                      └───────────┘ └───┘    └────────┘               
txt      └─────┘                      └───────────┘          └────────┘               
par      └─────┘                      └───────────┘          └────────┘               
pid      └───┘└┘                      └───────────┘          └────────┘               
st   ───────────────────────────────────────────────────────────────────────────────────────────
227        (I.inv_fun ⁻¹' (e.symm.trans e').source ∩ range I.to_fun).prod univ,
id          └───────┘      └──────────┘ └┘           └───┘ └──────┘       └──┘
src  ─────┘ └───────┘    └──────────┘  └───────┘ └───┘└──────┘└─────┘└──┘
typ  ─────┘ └───────┘    └──────────┘└┘└───────┘ └───┘└──────┘└─────┘└──┘
doc  ─────┘              └──────────┘  └───────┘ └───┘        └─────┘
txt  ─────┘                            └───────┘              └─────┘
par  ─────┘                            └───────┘              └─────┘
pid  ─────┘                            └───────┘              └─────┘
st   ────────────────────────────────────────────────────────────────────────┘└─
228      { have : range (λ (p : H × F), (I.to_fun (p.fst), id p.snd)) =
id                                               └──┘       └──┘
src        └─────┘       └────┘  └─┘          └──┘└─┘   └──┘└─┘ 
typ        └─────┘       └────┘ └─┘          └──┘└─┘   └──┘└─┘ 
doc        └─────┘       └────┘   └─┘               └─┘       └─┘ 
txt        └─────┘       └────┘   └─┘               └─┘       └─┘ 
par        └─────┘       └────┘   └─┘               └─┘       └─┘ 
pid        └───┘└┘       └────┘   └─┘               └─┘       └─┘ 
st   ─────┘└────────────────────────────────────────────────────────────
229               (range I.to_fun).prod (range (id : F → F)) := prod_range_range_eq.symm,
id                       └──────┘        └───┘  └┘             └──────────────────────┘
src  ────────────┘      └──────┘└─────┘ └───┘ └┘└─┘   └────┘└──────────────────────┘
typ  ────────────┘      └──────┘└─────┘ └───┘ └┘└─┘  └────┘└──────────────────────┘
doc  ────────────┘              └─────┘ └───┘   └─┘   └────┘
txt  ────────────┘              └─────┘         └─┘   └────┘
par  ────────────┘              └─────┘         └─┘   └────┘
pid  ────────────┘              └─────┘         └─┘   └┘└──┘
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
230        simp at this,
src        └──────────┘
typ        └──────────┘
doc        └──────────┘
txt        └──────────┘
par        └──────────┘
pid            └─────┘
st   ─────────────────┘└─
231        ext p,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
pid           └┘
st   ──────────┘└─
232        simp [-mem_range, J, local_equiv.trans_source, chart, model_with_corners.prod,
id                             └──────────────────────┘  └───┘  └─────────────────────┘
src        └────────────────┘ └┘└──────────────────────┘└┘└───┘└┘└─────────────────────┘└─
typ        └────────────────┘└┘└──────────────────────┘└┘└───┘└┘└─────────────────────┘└─
doc        └────────────────┘ └┘                        └┘└───┘└┘└─────────────────────┘└─
txt        └────────────────┘ └┘                        └┘     └┘                       └─
par        └────────────────┘ └┘                        └┘     └┘                       └─
pid            └───────────┘ └┘                        └┘     └┘                       └─
st   ─────────────────────────────────────────────────────────────────────────────────────
233              local_equiv.trans_target, this],
id               └──────────────────────┘  └──┘
src  ───────────┘└──────────────────────┘└┘    
typ  ───────────┘└──────────────────────┘└┘└──┘
doc  ───────────┘                        └┘    
txt  ───────────┘                        └┘    
par  ───────────┘                        └┘    
pid  ───────────┘                        └┘    
st   ──────────────────────────────────────────┘└─
234        split,
src        └───┘
typ        └───┘
doc        └───┘
txt        └───┘
par        └───┘
st   ──────────┘└─
235        { tauto },
src          └────┘
typ          └────┘
doc          └────┘
txt          └────┘
par          └────┘
pid               
st   ───────┘└────┘└┘
236        { exact λ⟨⟨hx1, hx2⟩, hx3⟩, ⟨⟨⟨hx1, e.map_target hx1⟩, hx2⟩, hx3⟩ } },
id                    └─┘  └─┘   └─┘           └──────────┘
src          └────┘     └┘   └─┘   └─┘      └┘└──────────┘   └─┘   └─┘   └┘
typ          └────┘  └─┘└┘└─┘└─┘└─┘└─┘      └┘└──────────┘   └─┘   └─┘   └┘
doc          └────┘     └┘   └─┘   └─┘      └┘               └─┘   └─┘   └┘
txt          └────┘     └┘   └─┘   └─┘      └┘               └─┘   └─┘   └┘
par          └────┘     └┘   └─┘   └─┘      └┘               └─┘   └─┘   └┘
pid                    └┘   └─┘   └─┘      └┘               └─┘   └─┘   
st   ───────────────────────────────────────────────────────────────────────┘└──┘
237      rw this,
id          └──┘
src      └─┘
typ      └─┘└──┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ──────────┘└─
238      -- check separately that the two components of the coordinate change are smooth
st   ────────────────────────────────────────────────────────────────────────────────────
239      apply times_cont_diff_on.prod _ _ U,
id             └─────────────────────┘     
src      └────┘└─────────────────────┘└───┘
typ      └────┘└─────────────────────┘└───┘
doc      └────┘└─────────────────────┘└───┘
txt      └────┘                       └───┘
par      └────┘                       └───┘
pid                                  └───┘
st   ──────────────────────────────────────┘└─
240      show times_cont_diff_on 𝕜 ⊤ (λ (p : E × F), (I.to_fun ∘ e'.to_fun ∘ e.inv_fun ∘ I.inv_fun) p.1)
id            └────────────────┘                              └───────┘   └───────┘
src      └───┘└────────────────┘    └────┘   └─┘          └───────┘ └───────┘          └┘ └───
typ      └───┘└────────────────┘   └────┘ └─┘          └───────┘ └───────┘          └┘ └───
doc      └───┘└────────────────┘    └────┘   └─┘                                       └┘ └───
txt      └───┘                      └────┘   └─┘                                       └┘ └───
par      └───┘                      └────┘   └─┘                                       └┘ └───
pid      └───┘                      └────┘   └─┘                                       └┘ └───
st   ────────────────────────────────────────────────────────────────────────────────────────────────────
241           ((I.inv_fun ⁻¹' (e.symm.trans e').source ∩ range I.to_fun).prod (univ : set F)),
id              └───────┘      └──────────┘ └┘           └───┘ └──────┘        └──┘   └─┘ 
src  ────────┘  └───────┘    └──────────┘  └───────┘ └───┘└──────┘└─────┘ └──┘└─┘└─┘ └┘
typ  ────────┘  └───────┘    └──────────┘└┘└───────┘ └───┘└──────┘└─────┘ └──┘└─┘└─┘└┘
doc  ────────┘               └──────────┘  └───────┘ └───┘        └─────┘     └─┘    └┘
txt  ────────┘                             └───────┘              └─────┘     └─┘    └┘
par  ────────┘                             └───────┘              └─────┘     └─┘    └┘
pid  ────────┘                             └───────┘              └─────┘     └─┘    └┘
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
242      { -- the coordinate change on the base is just a coordinate change for `M`, smooth since
st   ─────┘└──────────────────────────────────────────────────────────────────────────────────────
243        -- `M` is smooth
st   ───────────────────────
244        have A : times_cont_diff_on 𝕜 ⊤
id                  └────────────────┘ 
src        └───────┘└────────────────┘  
typ        └───────┘└────────────────┘ 
doc        └───────┘└────────────────┘  
txt        └───────┘                    
par        └───────┘                    
pid        └────┘└─┘                    
st   ──────────────────────────────────────
245          (I.to_fun ∘ (e.symm.trans e').to_fun ∘ I.inv_fun)
src  ───────┘                         └───────┘          └─
typ  ───────┘                         └───────┘          └─
doc  ───────┘                         └───────┘          └─
txt  ───────┘                         └───────┘          └─
par  ───────┘                         └───────┘          └─
pid  ───────┘                         └───────┘          └─
st   ──────────────────────────────────────────────────────────
246          (I.inv_fun ⁻¹' (e.symm.trans e').source ∩ range I.to_fun) :=
id            └───────┘      └──────────┘ └┘           └───┘ └──────┘
src  ───────┘ └───────┘    └──────────┘  └───────┘ └───┘└──────┘└────
typ  ───────┘ └───────┘    └──────────┘└┘└───────┘ └───┘└──────┘└────
doc  ───────┘              └──────────┘  └───────┘ └───┘        └────
txt  ───────┘                            └───────┘              └────
par  ───────┘                            └───────┘              └────
pid  ───────┘                            └───────┘              └───
st   ─────────────────────────────────────────────────────────────────────
247          (has_groupoid.compatible (times_cont_diff_groupoid ⊤ I) he he').1,
id            └─────────────────────┘  └──────────────────────┘     └┘ └─┘
src  ───────┘ └─────────────────────┘ └──────────────────────┘  └┘     └─┘
typ  ───────┘ └─────────────────────┘ └──────────────────────┘ └┘└┘└─┘└─┘
doc  ───────┘                         └──────────────────────┘  └┘     └─┘
txt  ───────┘                                                   └┘     └─┘
par  ───────┘                                                   └┘     └─┘
pid  ───────┘                                                   └┘     └┘
st   ────────────────────────────────────────────────────────────────────────┘└─
248        have B : times_cont_diff_on 𝕜 ⊤ (λp : E × F, p.1)
id                  └────────────────┘             
src        └───────┘└────────────────┘    └──┘   └┘ └───
typ        └───────┘└────────────────┘   └──┘ └┘ └───
doc        └───────┘└────────────────┘    └──┘   └┘ └───
txt        └───────┘                      └──┘   └┘ └───
par        └───────┘                      └──┘   └┘ └───
pid        └────┘└─┘                      └──┘   └┘ └───
st   ────────────────────────────────────────────────────────
249          ((I.inv_fun ⁻¹' (e.symm.trans e').source ∩ range I.to_fun).prod univ) :=
id             └───────┘      └──────────┘ └┘           └───┘ └──────┘       └──┘
src  ───────┘  └───────┘    └──────────┘  └───────┘ └───┘└──────┘└─────┘└──┘└────
typ  ───────┘  └───────┘    └──────────┘└┘└───────┘ └───┘└──────┘└─────┘└──┘└────
doc  ───────┘               └──────────┘  └───────┘ └───┘        └─────┘    └────
txt  ───────┘                             └───────┘              └─────┘    └────
par  ───────┘                             └───────┘              └─────┘    └────
pid  ───────┘                             └───────┘              └─────┘    └───
st   ─────────────────────────────────────────────────────────────────────────────────
250        times_cont_diff_fst.times_cont_diff_on U,
id         └────────────────────────────────────┘ 
src  ─────┘└────────────────────────────────────┘
typ  ─────┘└────────────────────────────────────┘
doc  ─────┘└────────────────────────────────────┘
txt  ─────┘                                      
par  ─────┘                                      
pid  ─────┘                                      
st   ─────────────────────────────────────────────┘└─
251        exact times_cont_diff_on.comp A B U (prod_subset_preimage_fst _ _) },
id               └─────────────────────┘     └──────────────────────┘
src        └────┘└─────────────────────┘    └──────────────────────┘└────┘
typ        └────┘└─────────────────────┘ └──────────────────────┘└────┘
doc        └────┘└─────────────────────┘                            └────┘
txt        └────┘                                                   └────┘
par        └────┘                                                   └────┘
pid                                                                └───┘
st   ────────────────────────────────────────────────────────────────────────┘└┘
252      show times_cont_diff_on 𝕜 ⊤ (λ (p : E × F),
id            └────────────────┘            
src      └───┘└────────────────┘    └────┘   └──
typ      └───┘└────────────────┘   └────┘  └──
doc      └───┘└────────────────┘    └────┘   └──
txt      └───┘                      └────┘   └──
par      └───┘                      └────┘   └──
pid      └───┘                      └────┘   └──
st   ────────────────────────────────────────────────
253        Z.coord_change ⟨chart_at H (e.inv_fun (I.inv_fun p.1)), _⟩ ⟨e', he'⟩
id                                                                         └─┘
src  ─────┘                                             └───────┘   └┘   └─
typ  ─────┘                                             └───────┘   └┘└─┘└─
doc  ─────┘                                             └───────┘   └┘   └─
txt  ─────┘                                             └───────┘   └┘   └─
par  ─────┘                                             └───────┘   └┘   └─
pid  ─────┘                                             └───────┘   └┘   └─
st   ───────────────────────────────────────────────────────────────────────────
254           ((chart_at H (e.inv_fun (I.inv_fun p.1))).to_fun (e.inv_fun (I.inv_fun p.1)))
src  ────────┘                                └───────────┘                     └─────
typ  ────────┘                                └───────────┘                     └─────
doc  ────────┘                                └───────────┘                     └─────
txt  ────────┘                                └───────────┘                     └─────
par  ────────┘                                └───────────┘                     └─────
pid  ────────┘                                └───────────┘                     └─────
st   ───────────────────────────────────────────────────────────────────────────────────────
255        (Z.coord_change ⟨e, he⟩ ⟨chart_at H (e.inv_fun (I.inv_fun p.1)), _⟩
id          └────────────┘     └┘   └──────┘ 
src  ─────┘ └────────────┘  └┘  └┘ └──────┘                      └────────
typ  ─────┘ └────────────┘  └┘└┘└┘ └──────┘                     └────────
doc  ─────┘                 └┘  └┘                               └────────
txt  ─────┘                 └┘  └┘                               └────────
par  ─────┘                 └┘  └┘                               └────────
pid  ─────┘                 └┘  └┘                               └────────
st   ──────────────────────────────────────────────────────────────────────────
256          (e.to_fun (e.inv_fun (I.inv_fun p.1))) p.2))
id            └──────┘  └───────┘
src  ───────┘ └──────┘ └───────┘           └────┘ └────
typ  ───────┘ └──────┘ └───────┘           └────┘ └────
doc  ───────┘                              └────┘ └────
txt  ───────┘                              └────┘ └────
par  ───────┘                              └────┘ └────
pid  ───────┘                              └────┘ └────
st   ─────────────────────────────────────────────────────
257        ((I.inv_fun ⁻¹' (e.symm.trans e').source ∩ range I.to_fun).prod (univ : set F)),
id           └───────┘      └──────────┘ └┘           └───┘ └──────┘        └──┘   └─┘ 
src  ─────┘  └───────┘    └──────────┘  └───────┘ └───┘└──────┘└─────┘ └──┘└─┘└─┘ └┘
typ  ─────┘  └───────┘    └──────────┘└┘└───────┘ └───┘└──────┘└─────┘ └──┘└─┘└─┘└┘
doc  ─────┘               └──────────┘  └───────┘ └───┘        └─────┘     └─┘    └┘
txt  ─────┘                             └───────┘              └─────┘     └─┘    └┘
par  ─────┘                             └───────┘              └─────┘     └─┘    └┘
pid  ─────┘                             └───────┘              └─────┘     └─┘    └┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
258      { /- The coordinate change in the fiber is more complicated as its definition involves the
st   ───────────────────────────────────────────────────────────────────────────────────────────────
259        reference chart chosen at each point. However, it appears with its inverse, so using the
st   ───────────────────────────────────────────────────────────────────────────────────────────────
260        cocycle property one can get rid of it, and then conclude using the smoothness of the
st   ────────────────────────────────────────────────────────────────────────────────────────────
261        cocycle as given in the definition of basic smooth bundles. -/
st   ─────────────────────────────────────────────────────────────────────
262        have := Z.coord_change_smooth ⟨e, he⟩ ⟨e', he'⟩,
id                 └───────────────────┘    └┘   └┘  └─┘
src        └──────┘└───────────────────┘  └┘  └┘   └┘   
typ        └──────┘└───────────────────┘ └┘└┘└┘ └┘└┘└─┘
doc        └──────┘                       └┘  └┘   └┘   
txt        └──────┘                       └┘  └┘   └┘   
par        └──────┘                       └┘  └┘   └┘   
pid        └───┘└─┘                       └┘  └┘   └┘   
st   ────────────────────────────────────────────────────┘└─
263        rw model_with_corners.image at this,
id            └──────────────────────┘
src        └─┘└──────────────────────┘└──────┘
typ        └─┘└──────────────────────┘└──────┘
doc        └─┘                        └──────┘
txt        └─┘                        └──────┘
par        └─┘                        └──────┘
pid                                  └──────┘
st   ────────────────────────────────────────┘└─
264        apply times_cont_diff_on.congr this U,
id               └──────────────────────┘ └──┘ 
src        └────┘└──────────────────────┘    
typ        └────┘└──────────────────────┘└──┘
doc        └────┘                            
txt        └────┘                            
par        └────┘                            
pid                                         
st   ──────────────────────────────────────────┘└─
265        rintros ⟨x, v⟩ hx,
src        └───────────────┘
typ        └───────────────┘
doc        └───────────────┘
txt        └───────────────┘
par        └───────────────┘
pid               └────────┘
st   ──────────────────────┘└─
266        simp [local_equiv.trans_source] at hx,
id               └──────────────────────┘
src        └────┘└──────────────────────┘└─────┘
typ        └────┘└──────────────────────┘└─────┘
doc        └────┘                        └─────┘
txt        └────┘                        └─────┘
par        └────┘                        └─────┘
pid                                    └───┘
st   ──────────────────────────────────────────┘└─
267        let f := chart_at H (e.inv_fun (I.inv_fun x)),
id                  └──────┘   └───────┘  └───────┘ 
src        └───────┘└──────┘  └───────┘ └───────┘ └┘
typ        └───────┘└──────┘ └───────┘ └───────┘└┘
doc        └───────┘                              └┘
txt        └───────┘                              └┘
par        └───────┘                              └┘
pid        └───┘└─┘                              └┘
st   ──────────────────────────────────────────────────┘└─
268        have A : I.inv_fun x ∈ ((e.symm.trans f).trans (f.symm.trans e')).source,
id                  └───────┘      └──────────┘           └──────────┘ └┘
src        └───────┘└───────┘    └──────────┘ └──────┘ └──────────┘  └───────┘
typ        └───────┘└───────┘   └──────────┘ └──────┘ └──────────┘└┘└───────┘
doc        └───────┘             └──────────┘ └──────┘ └──────────┘  └───────┘
txt        └───────┘                          └──────┘               └───────┘
par        └───────┘                          └──────┘               └───────┘
pid        └────┘└─┘                          └──────┘               └──────┘
st   ─────────────────────────────────────────────────────────────────────────────┘
269          by simp [local_equiv.trans_source, hx.1.1, hx.1.2, mem_chart_source, f.map_source],
id                    └──────────────────────┘  └┘      └┘      └──────────────┘
src             └────┘└──────────────────────┘└┘  └────┘  └────┘└──────────────┘└┘            
typ             └────┘└──────────────────────┘└┘└┘└────┘└┘└────┘└──────────────┘└┘└──────────┘
doc             └────┘                        └┘  └────┘  └────┘                └┘            
txt             └────┘                        └┘  └────┘  └────┘                └┘            
par             └────┘                        └┘  └────┘  └────┘                └┘            
pid                                         └┘  └────┘  └────┘                └┘            
st                                                                                             └─
270        rw e.right_inv hx.1.1,
id            └─────────┘ └┘
src        └─┘└─────────┘  └──┘
typ        └─┘└─────────┘└┘└──┘
doc        └─┘             └──┘
txt        └─┘             └──┘
par        └─┘             └──┘
pid                       └┘└┘
st   ──────────────────────────┘└─
271        have := Z.coord_change_comp ⟨e, he⟩ ⟨f, chart_mem_atlas _ _⟩ ⟨e', he'⟩ (I.inv_fun x) A v,
id                 └─────────────────┘    └┘     └─────────────┘       └┘  └─┘   └───────┘    
src        └──────┘└─────────────────┘  └┘  └┘  └┘└─────────────┘└────┘   └┘   └┘ └───────┘ └┘ 
typ        └──────┘└─────────────────┘ └┘└┘└┘ └┘└─────────────┘└────┘ └┘└┘└─┘└┘ └───────┘└┘
doc        └──────┘                     └┘  └┘  └┘               └────┘   └┘   └┘           └┘ 
txt        └──────┘                     └┘  └┘  └┘               └────┘   └┘   └┘           └┘ 
par        └──────┘                     └┘  └┘  └┘               └────┘   └┘   └┘           └┘ 
pid        └───┘└─┘                     └┘  └┘  └┘               └────┘   └┘   └┘           └┘ 
st   ─────────────────────────────────────────────────────────────────────────────────────────────┘└─
272        simpa using this } },
id                     └──┘
src        └──────────┘    
typ        └──────────┘└──┘
doc        └──────────┘    
txt        └──────────┘    
par        └──────────┘    
pid             └────┘    
st   ──────────────────────┘└──┘
273    haveI : has_groupoid Z.to_topological_fiber_bundle_core.total_space
id             └──────────┘ └────────────────────────────────────────────┘
src    └──────┘└──────────┘└────────────────────────────────────────────┘
typ    └──────┘└──────────┘└────────────────────────────────────────────┘
doc    └──────┘└──────────┘└────────────────────────────────────────────┘
txt    └──────┘                                                          
par    └──────┘                                                          
pid         └┘                                                          
st   ──────────────────────────────────────────────────────────────────────
274           (times_cont_diff_groupoid ⊤ (I.prod (model_with_corners_self 𝕜 F))) :=
id             └──────────────────────┘    └────┘  └─────────────────────┘  
src  ────────┘ └──────────────────────┘  └────┘ └─────────────────────┘  └──────
typ  ────────┘ └──────────────────────┘  └────┘ └─────────────────────┘└──────
doc  ────────┘ └──────────────────────┘  └────┘ └─────────────────────┘  └──────
txt  ────────┘                                                           └──────
par  ────────┘                                                           └──────
pid  ────────┘                                                           └─┘└───
st   ────────────────────────────────────────────────────────────────────────────────
275    begin
src  ─┘     
typ  ─┘     
doc  ─┘     
txt  ─┘     
par  ─┘     
pid  ─┘     
st   ─┘└─────
276      split,
src  ───┘└───┘└─
typ  ───┘└───┘└─
doc  ───┘└───┘└─
txt  ───┘└───┘└─
par  ───┘└───┘└─
pid  ───────────
st   ────────┘└─
277      assume e₀ e₀' he₀ he₀',
src  ───┘└────────────────────┘└─
typ  ───┘└────────────────────┘└─
doc  ───┘└────────────────────┘└─
txt  ───┘└────────────────────┘└─
par  ───┘└────────────────────┘└─
pid  ────────────────────────────
st   ─────────────────────────┘└─
278      rcases (Z.mem_atlas_iff _).1 he₀ with ⟨e, he, rfl⟩,
id               └─────────────┘      └─┘
src  ───┘└─────┘ └─────────────┘└────┘   └────────────────┘└─
typ  ───┘└─────┘ └─────────────┘└────┘└─┘└────────────────┘└─
doc  ───┘└─────┘                └────┘   └────────────────┘└─
txt  ───┘└─────┘                └────┘   └────────────────┘└─
par  ───┘└─────┘                └────┘   └────────────────┘└─
pid  ──────────┘                └────┘   └───────────────────
st   ─────────────────────────────────────────────────────┘└─
279      rcases (Z.mem_atlas_iff _).1 he₀' with ⟨e', he', rfl⟩,
id               └─────────────┘      └──┘
src  ───┘└─────┘ └─────────────┘└────┘    └──────────────────┘└─
typ  ───┘└─────┘ └─────────────┘└────┘└──┘└──────────────────┘└─
doc  ───┘└─────┘                └────┘    └──────────────────┘└─
txt  ───┘└─────┘                └────┘    └──────────────────┘└─
par  ───┘└─────┘                └────┘    └──────────────────┘└─
pid  ──────────┘                └────┘    └─────────────────────
st   ────────────────────────────────────────────────────────┘└─
280      rw [times_cont_diff_groupoid, mem_groupoid_of_pregroupoid],
id           └──────────────────────┘  └─────────────────────────┘
src  ───┘└──┘└──────────────────────┘└┘└─────────────────────────┘└─
typ  ───┘└──┘└──────────────────────┘└┘└─────────────────────────┘└─
doc  ───┘└──┘└──────────────────────┘└┘                           └─
txt  ───┘└──┘                        └┘                           └─
par  ───┘└──┘                        └┘                           └─
pid  ───────┘                        └┘                           └──
st   ───────────────────────────────┘└───────────────────────────┘└──
281      exact ⟨A e e' he he', A e' e he' he⟩
id                              └┘  └─┘ └┘
src  ───┘└────┘          └┘         └─
typ  ───┘└────┘          └┘└┘└─┘└┘└─
doc  ───┘└────┘          └┘         └─
txt  ───┘└────┘          └┘         └─
par  ───┘└────┘          └┘         └─
pid  ─────────┘          └┘         └─
st   ─────────────────────────────────────────
282    end,
src  ─┘└─┘
typ  ─┘└─┘
doc  ─┘└─┘
txt  ─┘└─┘
par  ─┘└─┘
pid  ────┘
st   ─┘└─┘└─
283    constructor
src    └──────────┘
typ    └──────────┘
doc    └──────────┘
txt    └──────────┘
par    └──────────┘
pid               
st   ─────────────┘
284  end
st   └─┘
285  
286  end basic_smooth_bundle_core
287  
288  section tangent_bundle
289  
290  variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
id                         └──────────────────────┘
src                         └──────────────────────┘
typ                        └──────────────────────┘
doc                         └──────────────────────┘
291  {E : Type u} [normed_group E] [normed_space 𝕜 E]
id                 └──────────┘     └──────────┘
src                └──────────┘     └──────────┘
typ                └──────────┘     └──────────┘
doc                └──────────┘     └──────────┘
292  {H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
id                └───────────────┘         └────────────────┘
src               └───────────────┘         └────────────────┘
typ               └───────────────┘         └────────────────┘
doc               └───────────────┘         └────────────────┘
293  (M : Type*) [topological_space M] [manifold H M] [smooth_manifold_with_corners I M]
id                └───────────────┘     └──────┘       └──────────────────────────┘
src               └───────────────┘     └──────┘       └──────────────────────────┘
typ               └───────────────┘     └──────┘       └──────────────────────────┘
doc               └───────────────┘     └──────┘       └──────────────────────────┘
294  
295  set_option class.instance_max_depth 50
doc             └──────────────────────┘
296  
297  /-- Basic smooth bundle core version of the tangent bundle of a smooth manifold `M` modelled over a
298  model with corners `I` on `(E, H)`. The fibers are equal to `E`, and the coordinate change in the
299  fiber corresponds to the derivative of the coordinate change in `M`. -/
300  def tangent_bundle_core : basic_smooth_bundle_core I M E :=
id                             └──────────────────────┘   
src                            └──────────────────────┘
typ                            └──────────────────────┘   
doc                            └──────────────────────┘
301  { coord_change := λi j x v, (fderiv_within 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id                            └───────────┘   └─────┘   └────┘    └─────┘   └──────┘
src                               └───────────┘     └─────┘    └────┘     └─────┘    └──────┘
typ                           └───────────┘   └─────┘   └────┘    └─────┘   └──────┘
doc                               └───────────┘
302                              (range I.to_fun) (I.to_fun x) : E → E) v,
id                                └───┘ └─────┘   └─────┘          
src                               └───┘  └─────┘    └─────┘
typ                               └───┘ └─────┘   └─────┘          
doc                               └───┘
303    coord_change_smooth := λi j, begin
id                              
typ                             
st                                  └─────
304      /- To check that the coordinate change of the bundle is smooth, one should just use the
st   ────────────────────────────────────────────────────────────────────────────────────────────
305      smoothness of the charts, and thus the smoothness of their derivatives. -/
st   ───────────────────────────────────────────────────────────────────────────────
306      rw model_with_corners.image,
id          └──────────────────────┘
src      └─┘└──────────────────────┘
typ      └─┘└──────────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ──────────────────────────────┘└─
307      have A : times_cont_diff_on 𝕜 ⊤
id                └────────────────┘ 
src      └───────┘└────────────────┘  
typ      └───────┘└────────────────┘ 
doc      └───────┘└────────────────┘  
txt      └───────┘                    
par      └───────┘                    
pid      └────┘└─┘                    
st   ────────────────────────────────────
308        (I.to_fun ∘ (i.1.symm.trans j.1).to_fun ∘ I.inv_fun)
src  ─────┘            └────────────┘ └─────────┘          └─
typ  ─────┘            └────────────┘ └─────────┘          └─
doc  ─────┘            └────────────┘ └─────────┘          └─
txt  ─────┘            └────────────┘ └─────────┘          └─
par  ─────┘            └────────────┘ └─────────┘          └─
pid  ─────┘            └────────────┘ └─────────┘          └─
st   ───────────────────────────────────────────────────────────
309        (I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∩ range I.to_fun) :=
id          └───────┘                                 └───┘ └──────┘
src  ─────┘ └───────┘     └────────────┘ └─────────┘ └───┘└──────┘└────
typ  ─────┘ └───────┘    └────────────┘└─────────┘ └───┘└──────┘└────
doc  ─────┘               └────────────┘ └─────────┘ └───┘        └────
txt  ─────┘               └────────────┘ └─────────┘              └────
par  ─────┘               └────────────┘ └─────────┘              └────
pid  ─────┘               └────────────┘ └─────────┘              └───
st   ──────────────────────────────────────────────────────────────────────
310        (has_groupoid.compatible (times_cont_diff_groupoid ⊤ I) i.2 j.2).1,
id          └─────────────────────┘  └──────────────────────┘        
src  ─────┘ └─────────────────────┘ └──────────────────────┘  └┘ └─┘ └───┘
typ  ─────┘ └─────────────────────┘ └──────────────────────┘ └┘└─┘└───┘
doc  ─────┘                         └──────────────────────┘  └┘ └─┘ └───┘
txt  ─────┘                                                   └┘ └─┘ └───┘
par  ─────┘                                                   └┘ └─┘ └───┘
pid  ─────┘                                                   └┘ └─┘ └─┘└┘
st   ───────────────────────────────────────────────────────────────────────┘└─
311      have B : unique_diff_on 𝕜 (I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∩ range I.to_fun),
id                └────────────┘   └───────┘                                 └───┘ └──────┘
src      └───────┘└────────────┘  └───────┘     └────────────┘ └─────────┘ └───┘└──────┘
typ      └───────┘└────────────┘ └───────┘    └────────────┘└─────────┘ └───┘└──────┘
doc      └───────┘└────────────┘                └────────────┘ └─────────┘ └───┘        
txt      └───────┘                              └────────────┘ └─────────┘              
par      └───────┘                              └────────────┘ └─────────┘              
pid      └────┘└─┘                              └────────────┘ └─────────┘              
st   ─────────────────────────────────────────────────────────────────────────────────────────┘└─
312      { rw inter_comm,
id            └────────┘
src        └─┘└────────┘
typ        └─┘└────────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ─────┘└───────────┘└─
313        apply I.unique_diff.inter (I.continuous_inv_fun _ (local_homeomorph.open_source _)) },
id               └─────────────────┘  └──────────────────┘    └──────────────────────────┘
src        └────┘└─────────────────┘ └──────────────────┘└─┘ └──────────────────────────┘└───┘
typ        └────┘└─────────────────┘ └──────────────────┘└─┘ └──────────────────────────┘└───┘
doc        └────┘                                        └─┘                             └───┘
txt        └────┘                                        └─┘                             └───┘
par        └────┘                                        └─┘                             └───┘
pid                                                     └─┘                             └──┘
st   ─────────────────────────────────────────────────────────────────────────────────────────┘└┘
314      have C : times_cont_diff_on 𝕜 ⊤
id                └────────────────┘
src      └───────┘└────────────────┘  
typ      └───────┘└────────────────┘  
doc      └───────┘└────────────────┘  
txt      └───────┘                    
par      └───────┘                    
pid      └────┘└─┘                    
st   ────────────────────────────────────
315        (λ (p : E × E), (fderiv_within 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id                         └───────────┘ 
src  ─────┘  └────┘  └─┘ └───────────┘            └────────┘  └─────────┘          └─
typ  ─────┘  └────┘  └─┘ └───────────┘           └────────┘  └─────────┘          └─
doc  ─────┘  └────┘   └─┘ └───────────┘            └────────┘  └─────────┘          └─
txt  ─────┘  └────┘   └─┘                          └────────┘  └─────────┘          └─
par  ─────┘  └────┘   └─┘                          └────────┘  └─────────┘          └─
pid  ─────┘  └────┘   └─┘                          └────────┘  └─────────┘          └─
st   ─────────────────────────────────────────────────────────────────────────────────────────
316              (I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∩ range I.to_fun) p.1 : E → E) p.2)
id                                                                                      
src  ───────────┘               └────────────┘ └─────────┘              └┘ └───┘   └┘ └───
typ  ───────────┘               └────────────┘ └─────────┘              └┘ └───┘  └┘ └───
doc  ───────────┘               └────────────┘ └─────────┘              └┘ └───┘   └┘ └───
txt  ───────────┘               └────────────┘ └─────────┘              └┘ └───┘   └┘ └───
par  ───────────┘               └────────────┘ └─────────┘              └┘ └───┘   └┘ └───
pid  ───────────┘               └────────────┘ └─────────┘              └┘ └───┘   └┘ └───
st   ───────────────────────────────────────────────────────────────────────────────────────────
317        ((I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∩ range I.to_fun).prod univ) :=
id           └───────┘                                 └───┘ └──────┘       └──┘
src  ─────┘  └───────┘     └────────────┘ └─────────┘ └───┘└──────┘└─────┘└──┘└────
typ  ─────┘  └───────┘    └────────────┘└─────────┘ └───┘└──────┘└─────┘└──┘└────
doc  ─────┘                └────────────┘ └─────────┘ └───┘        └─────┘    └────
txt  ─────┘                └────────────┘ └─────────┘              └─────┘    └────
par  ─────┘                └────────────┘ └─────────┘              └─────┘    └────
pid  ─────┘                └────────────┘ └─────────┘              └─────┘    └───
st   ──────────────────────────────────────────────────────────────────────────────────
318        times_cont_diff_on_fderiv_within_apply A B lattice.le_top,
id         └────────────────────────────────────┘   └────────────┘
src  ─────┘└────────────────────────────────────┘  └────────────┘
typ  ─────┘└────────────────────────────────────┘└────────────┘
doc  ─────┘└────────────────────────────────────┘  
txt  ─────┘                                        
par  ─────┘                                        
pid  ─────┘                                        
st   ──────────────────────────────────────────────────────────────┘└─
319      have D : ∀ x ∈ (I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∩ range I.to_fun),
src      └───────┘ └───┘               └────────────┘ └─────────┘               
typ      └───────┘ └───┘               └────────────┘ └─────────┘               
doc      └───────┘ └───┘               └────────────┘ └─────────┘               
txt      └───────┘ └───┘               └────────────┘ └─────────┘               
par      └───────┘ └───┘               └────────────┘ └─────────┘               
pid      └────┘└─┘ └───┘               └────────────┘ └─────────┘               
st   ─────────────────────────────────────────────────────────────────────────────────
320        fderiv_within 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
src  ─────┘                         └────────┘  └─────────┘          └─
typ  ─────┘                         └────────┘  └─────────┘          └─
doc  ─────┘                         └────────┘  └─────────┘          └─
txt  ─────┘                         └────────┘  └─────────┘          └─
par  ─────┘                         └────────┘  └─────────┘          └─
pid  ─────┘                         └────────┘  └─────────┘          └─
st   ────────────────────────────────────────────────────────────────────────
321              (range I.to_fun) x =
src  ───────────┘              └┘  
typ  ───────────┘              └┘  
doc  ───────────┘              └┘  
txt  ───────────┘              └┘  
par  ───────────┘              └┘  
pid  ───────────┘              └┘  
st   ─────────────────────────────────
322        fderiv_within 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id         └───────────┘ 
src  ─────┘└───────────┘            └────────┘  └─────────┘          └─
typ  ─────┘└───────────┘           └────────┘  └─────────┘          └─
doc  ─────┘└───────────┘            └────────┘  └─────────┘          └─
txt  ─────┘                         └────────┘  └─────────┘          └─
par  ─────┘                         └────────┘  └─────────┘          └─
pid  ─────┘                         └────────┘  └─────────┘          └─
st   ────────────────────────────────────────────────────────────────────────
323              (I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∩ range I.to_fun) x,
id                └───────┘                                 └───┘ └──────┘
src  ───────────┘ └───────┘     └────────────┘ └─────────┘ └───┘└──────┘└┘
typ  ───────────┘ └───────┘    └────────────┘└─────────┘ └───┘└──────┘└┘
doc  ───────────┘               └────────────┘ └─────────┘ └───┘        └┘
txt  ───────────┘               └────────────┘ └─────────┘              └┘
par  ───────────┘               └────────────┘ └─────────┘              └┘
pid  ───────────┘               └────────────┘ └─────────┘              └┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
324      { assume x hx,
src        └─────────┘
typ        └─────────┘
doc        └─────────┘
txt        └─────────┘
par        └─────────┘
pid        └─────────┘
st   ─────┘└─────────┘└─
325        have N : I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∈ nhds x :=
id                  └───────┘                                 └──┘ 
src        └───────┘└───────┘     └────────────┘ └─────────┘ └──┘ └───
typ        └───────┘└───────┘    └────────────┘└─────────┘ └──┘└───
doc        └───────┘              └────────────┘ └─────────┘ └──┘ └───
txt        └───────┘              └────────────┘ └─────────┘      └───
par        └───────┘              └────────────┘ └─────────┘      └───
pid        └────┘└─┘              └────────────┘ └─────────┘      └───
st   ─────────────────────────────────────────────────────────────────────
326          I.continuous_inv_fun.continuous_at.preimage_mem_nhds
id           └──────────────────────────────────────────────────┘
src  ───────┘└──────────────────────────────────────────────────┘
typ  ───────┘└──────────────────────────────────────────────────┘
doc  ───────┘                                                    
txt  ───────┘                                                    
par  ───────┘                                                    
pid  ───────┘                                                    
st   ─────────────────────────────────────────────────────────────
327            (mem_nhds_sets (local_homeomorph.open_source _) hx.1),
id              └───────────┘  └──────────────────────────┘    └┘
src  ─────────┘ └───────────┘ └──────────────────────────┘└──┘  └─┘
typ  ─────────┘ └───────────┘ └──────────────────────────┘└──┘└┘└─┘
doc  ─────────┘                                           └──┘  └─┘
txt  ─────────┘                                           └──┘  └─┘
par  ─────────┘                                           └──┘  └─┘
pid  ─────────┘                                           └──┘  └─┘
st   ──────────────────────────────────────────────────────────────┘└─
328        symmetry,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
st   ─────────────┘└─
329        rw inter_comm,
id            └────────┘
src        └─┘└────────┘
typ        └─┘└────────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ──────────────────┘└─
330        exact fderiv_within_inter N (I.unique_diff _ hx.2) },
id               └─────────────────┘   └───────────┘   └┘
src        └────┘└─────────────────┘  └───────────┘└─┘  └──┘
typ        └────┘└─────────────────┘ └───────────┘└─┘└┘└──┘
doc        └────┘                                  └─┘  └──┘
txt        └────┘                                  └─┘  └──┘
par        └────┘                                  └─┘  └──┘
pid                                               └─┘  └─┘
st   ────────────────────────────────────────────────────────┘└┘
331      apply times_cont_diff_on.congr C (unique_diff_on.prod B unique_diff_on_univ),
id             └──────────────────────┘   └─────────────────┘  └─────────────────┘
src      └────┘└──────────────────────┘  └─────────────────┘ └─────────────────┘
typ      └────┘└──────────────────────┘ └─────────────────┘└─────────────────┘
doc      └────┘                          └─────────────────┘                    
txt      └────┘                                                                 
par      └────┘                                                                 
pid                                                                            
st   ───────────────────────────────────────────────────────────────────────────────┘└─
332      rintros ⟨x, v⟩ hx,
src      └───────────────┘
typ      └───────────────┘
doc      └───────────────┘
txt      └───────────────┘
par      └───────────────┘
pid             └────────┘
st   ────────────────────┘
333      have E : x ∈ I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∩ range I.to_fun,
334        by simpa using hx,
id                        └┘
src           └──────────┘
typ           └──────────┘└┘
doc           └──────────┘
txt           └──────────┘
par           └──────────┘
pid                └────┘
335      have : I.to_fun (I.inv_fun x) = x, by simp [E.2],
id                                                   
src                                            └────┘ └─┘
typ                                            └────┘└─┘
doc                                            └────┘ └─┘
txt                                            └────┘ └─┘
par                                            └────┘ └─┘
pid                                                 └─┘
336      dsimp,
337      rw [this, D x E],
338      refl
339    end,
st     └─┘
340    coord_change_self := λi x hx v, begin
id                             └┘ 
typ                            └┘ 
st                                     └─────
341      /- Locally, a self-change of coordinate is just the identity, thus its derivative is the
st   ─────────────────────────────────────────────────────────────────────────────────────────────
342      identity. One just needs to write this carefully, paying attention to the sets where the
st   ─────────────────────────────────────────────────────────────────────────────────────────────
343      functions are defined. -/
st   ──────────────────────────────
344      have A : I.inv_fun ⁻¹' (i.1.symm.trans i.1).source ∩ range I.to_fun ∈
id                └───────┘ └─┘                                            
src      └───────┘└───────┘└─┘  └────────────┘ └─────────┘             
typ      └───────┘└───────┘└─┘  └────────────┘└─────────┘             
doc      └───────┘         └─┘  └────────────┘ └─────────┘               
txt      └───────┘              └────────────┘ └─────────┘               
par      └───────┘              └────────────┘ └─────────┘               
pid      └────┘└─┘              └────────────┘ └─────────┘               
st   ──────────────────────────────────────────────────────────────────────────
345        nhds_within (I.to_fun x) (range I.to_fun),
id         └─────────┘              └───┘ └──────┘
src  ─────┘└─────────┘          └┘ └───┘└──────┘
typ  ─────┘└─────────┘         └┘ └───┘└──────┘
doc  ─────┘└─────────┘          └┘ └───┘        
txt  ─────┘                     └┘              
par  ─────┘                     └┘              
pid  ─────┘                     └┘              
st   ──────────────────────────────────────────────┘└─
346      { rw inter_comm,
id            └────────┘
src        └─┘└────────┘
typ        └─┘└────────┘
doc        └─┘
txt        └─┘
par        └─┘
pid          
st   ────┘ └───────────┘ 
347        apply inter_mem_nhds_within,
id               └───────────────────┘
src        └────┘└───────────────────┘
typ        └────┘└───────────────────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ────────────────────────────────┘└─
348        apply I.continuous_inv_fun.continuous_at.preimage_mem_nhds
id               └──────────────────────────────────────────────────┘
src        └────┘└──────────────────────────────────────────────────┘
typ        └────┘└──────────────────────────────────────────────────┘
doc        └────┘                                                    
txt        └────┘                                                    
par        └────┘                                                    
pid                                                                 
st   ─────────────────────────────────────────────────────────────────
349          (mem_nhds_sets (local_homeomorph.open_source _) _),
id            └───────────┘  └──────────────────────────┘
src  ───────┘ └───────────┘ └──────────────────────────┘└────┘
typ  ───────┘ └───────────┘ └──────────────────────────┘└────┘
doc  ───────┘                                           └────┘
txt  ───────┘                                           └────┘
par  ───────┘                                           └────┘
pid  ───────┘                                           └────┘
st   ─────────────────────────────────────────────────────────┘└┘
350        simp [hx, local_equiv.trans_source, i.1.map_target] },
st                                                             └┘
351      have B : ∀ᶠ y in nhds_within (I.to_fun x) (range I.to_fun),
id                                             
typ                                            
352        (I.to_fun ∘ i.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun) y = (id : E → E) y,
id                                                                         
typ                                                                        
353      { apply filter.mem_sets_of_superset A,
354        assume y hy,
355        rw ← model_with_corners.image at hy,
356        rcases hy with ⟨z, hz⟩,
357        simp [local_equiv.trans_source] at hz,
358        simp [hz.2.symm, hz.1] },
st                                └┘
359      have C : fderiv_within 𝕜 (I.to_fun ∘ i.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
360                 (range I.to_fun) (I.to_fun x) =
361               fderiv_within 𝕜 (id : E → E) (range I.to_fun) (I.to_fun x) :=
id                                                                      
typ                                                                     
362        fderiv_within_congr_of_mem_nhds_within (I.unique_diff _ (mem_range_self _)) B (by simp [hx]),
363      rw fderiv_within_id (I.unique_diff _ (mem_range_self _)) at C,
364      rw C,
365      refl
366    end,
st     └─┘
367    coord_change_comp := λi j u x hx, begin
id                                 
typ                                
368      /- The cocycle property is just the fact that the derivative of a composition is the product of
369      the derivatives. One needs however to check that all the functions one considers are smooth, and
370      to pay attention to the domains where these functions are defined, making this proof a little
371      bit cumbersome although there is nothing complicated here. -/
372      have M : I.to_fun x ∈
id                         
typ                        
373        (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun) :=
374      ⟨by simpa using hx, mem_range_self _⟩,
375      have U : unique_diff_within_at 𝕜
id                                      
typ                                     
376        (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
377        (I.to_fun x),
id                   
typ                  
378      { have : unique_diff_on 𝕜
id                               
typ                              
379          (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun),
380        { rw inter_comm,
381          exact I.unique_diff.inter (I.continuous_inv_fun _ (local_homeomorph.open_source _)) },
st                                                                                               └┘
382        exact this _ M },
st                        └┘
383      have A : fderiv_within 𝕜 ((I.to_fun ∘ u.1.to_fun ∘ j.1.inv_fun ∘ I.inv_fun)
384                            ∘ (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun))
385               (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
386               (I.to_fun x)
387        = (fderiv_within 𝕜 (I.to_fun ∘ u.1.to_fun ∘ j.1.inv_fun ∘ I.inv_fun)
388               (I.inv_fun ⁻¹' (j.1.symm.trans u.1).source ∩ range I.to_fun)
389               ((I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun) (I.to_fun x))).comp
390          (fderiv_within 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id                          
typ                         
391               (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
392               (I.to_fun x)),
id                          
typ                         
393      { apply fderiv_within.comp _ _ _ _ U,
394        show differentiable_within_at 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id                                       
typ                                      
395          (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
396          (I.to_fun x),
id                     
typ                    
397        { have A : times_cont_diff_on 𝕜 ⊤
id                                       
typ                                      
398            (I.to_fun ∘ (i.1.symm.trans j.1).to_fun ∘ I.inv_fun)
399            (I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∩ range I.to_fun) :=
400          (has_groupoid.compatible (times_cont_diff_groupoid ⊤ I) i.2 j.2).1,
401          have B : differentiable_on 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id                                      
typ                                     
402            (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun),
403          { apply (A.differentiable_on (lattice.le_top)).mono,
404            have : ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ⊆ (i.1.symm.trans j.1).source :=
405              inter_subset_left _ _,
406            exact inter_subset_inter (preimage_mono this) (subset.refl (range I.to_fun)) },
st                                                                                          └┘
407          apply B,
408          simpa [mem_inter_iff, -mem_image, -mem_range, mem_range_self] using hx },
st                                                                                  └┘
409        show differentiable_within_at 𝕜 (I.to_fun ∘ u.1.to_fun ∘ j.1.inv_fun ∘ I.inv_fun)
id                                       
typ                                      
410          (I.inv_fun ⁻¹' (j.1.symm.trans u.1).source ∩ range I.to_fun)
411          ((I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun) (I.to_fun x)),
id                                                                        
typ                                                                       
412        { have A : times_cont_diff_on 𝕜 ⊤
id                                       
typ                                      
413            (I.to_fun ∘ (j.1.symm.trans u.1).to_fun ∘ I.inv_fun)
414            (I.inv_fun ⁻¹' (j.1.symm.trans u.1).source ∩ range I.to_fun) :=
415          (has_groupoid.compatible (times_cont_diff_groupoid ⊤ I) j.2 u.2).1,
416          apply A.differentiable_on (lattice.le_top),
417          rw [local_homeomorph.trans_source] at hx,
418          simp [mem_inter_iff, -mem_image, -mem_range, mem_range_self],
419          exact hx.2 },
st                      └┘
420        show (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
421          ⊆ (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun) ⁻¹'
422            (I.inv_fun ⁻¹' (j.1.symm.trans u.1).source ∩ range I.to_fun),
423        { assume y hy,
424          simp [-mem_range, local_equiv.trans_source] at hy,
425          rw [local_equiv.left_inv] at hy,
426          { simp [-mem_range, mem_range_self, hy, local_equiv.trans_source] },
st                                                                             └┘
427          { exact hy.1.1.2 } } },
st                            └────┘
428      have B : fderiv_within 𝕜 ((I.to_fun ∘ u.1.to_fun ∘ j.1.inv_fun ∘ I.inv_fun)
429                            ∘ (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun))
430               (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
431               (I.to_fun x)
432               = fderiv_within 𝕜 (I.to_fun ∘ u.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id                                
typ                               
433               (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
434               (I.to_fun x),
id                          
typ                         
435      { have E : ∀ y ∈ (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun),
436          ((I.to_fun ∘ u.1.to_fun ∘ j.1.inv_fun ∘ I.inv_fun)
437                            ∘ (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)) y =
438          (I.to_fun ∘ u.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun) y,
439        { assume y hy,
440          simp only [function.comp_app, model_with_corners_left_inv],
441          rw [j.1.left_inv],
442          exact hy.1.1.2 },
st                          └┘
443        exact fderiv_within_congr U E (E _ M) },
st                                               └┘
444      have C : fderiv_within 𝕜 (I.to_fun ∘ u.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
445               (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
446               (I.to_fun x) =
447               fderiv_within 𝕜 (I.to_fun ∘ u.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id                              
typ                             
448               (range I.to_fun) (I.to_fun x),
id                                           
typ                                          
449      { rw inter_comm,
450        apply fderiv_within_inter _ (I.unique_diff _ (mem_range_self _)),
451        apply I.continuous_inv_fun.continuous_at.preimage_mem_nhds
452          (mem_nhds_sets (local_homeomorph.open_source _) _),
453        simpa using hx },
st                        └┘
454      have D : fderiv_within 𝕜 (I.to_fun ∘ u.1.to_fun ∘ j.1.inv_fun ∘ I.inv_fun)
455                 (I.inv_fun ⁻¹' (j.1.symm.trans u.1).source ∩ range I.to_fun)
456                 ((I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun) (I.to_fun x)) =
457               fderiv_within 𝕜 (I.to_fun ∘ u.1.to_fun ∘ j.1.inv_fun ∘ I.inv_fun)
id                              
typ                             
458                 (range I.to_fun)
459                 ((I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun) (I.to_fun x)),
id                                                                               
typ                                                                              
460      { rw inter_comm,
461        apply fderiv_within_inter _ (I.unique_diff _ (mem_range_self _)),
462        apply I.continuous_inv_fun.continuous_at.preimage_mem_nhds
463          (mem_nhds_sets (local_homeomorph.open_source _) _),
464        rw [local_homeomorph.trans_source] at hx,
465        simp [mem_inter_iff, -mem_image, -mem_range, mem_range_self],
466        exact hx.2 },
st                    └┘
467      have E : fderiv_within 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
468                 (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
469                 (I.to_fun x) =
470               (fderiv_within 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id                               
typ                              
471                 (range I.to_fun)
472                 (I.to_fun x)),
id                            
typ                           
473      { rw inter_comm,
474        apply fderiv_within_inter _ (I.unique_diff _ (mem_range_self _)),
475        apply I.continuous_inv_fun.continuous_at.preimage_mem_nhds
476          (mem_nhds_sets (local_homeomorph.open_source _) _),
477        simpa using hx },
st                        └┘
478      rw [B, C, D, E] at A,
479      rw A,
480      assume v,
481      simp,
482      unfold_coes,
483      simp
484    end }
st     └─┘
485  
486  /-- The tangent bundle to a smooth manifold, as a plain type. -/
487  def tangent_bundle := (tangent_bundle_core I M).to_topological_fiber_bundle_core.total_space
id                                                
typ                                               
488  
489  /-- The projection from the tangent bundle of a smooth manifold to the manifold. As the tangent
490  bundle is represented internally as a product type, the notation `p.1` also works for the projection
491  of the point `p`. -/
492  def tangent_bundle.proj : tangent_bundle I M → M :=
id                                                 
typ                                                
493  (tangent_bundle_core I M).to_topological_fiber_bundle_core.proj
id                          
typ                         
494  
495  variable {M}
496  
497  /-- The tangent space at a point of the manifold `M`. It is just `E`. -/
498  def tangent_space (x : M) : Type* :=
id                          
typ                         
499  (tangent_bundle_core I M).to_topological_fiber_bundle_core.fiber x
id                                                                   
typ                                                                  
500  
501  section tangent_bundle_instances
502  
503  /- In general, the definition of tangent_bundle and tangent_space are not reducible, so that type
504  class inference does not pick wrong instances. In this section, we record the right instances for
505  them, noting in particular that the tangent bundle is a smooth manifold. -/
506  variable (M)
507  local attribute [reducible] tangent_bundle
doc                   └───────┘
508  
509  instance : topological_space (tangent_bundle I M) := by apply_instance
id                                                  
typ                                                 
510  instance : manifold (H × E) (tangent_bundle I M) := by apply_instance
id                                               
typ                                              
511  instance : smooth_manifold_with_corners I.tangent (tangent_bundle I M) := by apply_instance
id                                                                       
typ                                                                      
512  
513  local attribute [reducible] tangent_space topological_fiber_bundle_core.fiber
doc                   └───────┘
514  /- When `topological_fiber_bundle_core.fiber` is reducible, then
515  `topological_fiber_bundle_core.topological_space_fiber` can be applied to prove that any space is
516  a topological space, with several unknown metavariables. This is a bad instance, that we disable.-/
517  local attribute [instance, priority 0] topological_fiber_bundle_core.topological_space_fiber
518  
519  variables {M} (x : M)
520  
521  instance : topological_module 𝕜 (tangent_space I x) := by apply_instance
id                                                   
typ                                                  
522  instance : topological_space (tangent_space I x) := by apply_instance
id              └┘  └┘  └┘  └┘                    
src             └┘  └┘  └┘  └┘  
typ             └┘  └┘  └┘  └┘                    
doc             └┘  └┘  └┘  └┘  
523  instance : add_comm_group (tangent_space I x) := by apply_instance
id              └┘  └┘  └┘  └┘                  
src             └┘  └┘  └┘  └┘
typ             └┘  └┘  └┘  └┘                  
524  instance : topological_add_group (tangent_space I x) := by apply_instance
id                                                     
typ                                                    
525  instance : vector_space 𝕜 (tangent_space I x) := by apply_instance
id                                             
typ                                            
526  
527  end tangent_bundle_instances
528  
529  variable (M)
530  
531  /-- The tangent bundle projection on the basis is a continuous map. -/
532  lemma tangent_bundle_proj_continuous : continuous (tangent_bundle.proj I M) :=
id                                                                            
typ                                                                           
533  topological_fiber_bundle_core.continuous_proj _
534  
535  /-- The tangent bundle projection on the basis is an open map. -/
536  lemma tangent_bundle_proj_open : is_open_map (tangent_bundle.proj I M) :=
id                                                                       
typ                                                                      
537  topological_fiber_bundle_core.is_open_map_proj _
538  
539  /-- In the tangent bundle to the model space, the charts are just the identity-/
540  @[simp] lemma tangent_bundle_model_space_chart_at (p : tangent_bundle I H) :
id                                                                           
typ                                                                          
doc    └──┘
541    (chart_at (H × E) p).to_local_equiv = local_equiv.refl (H × E) :=
id                                                              
typ                                                             
542  begin
543    have A : ∀ x_fst, fderiv_within 𝕜 (I.to_fun ∘ I.inv_fun) (range I.to_fun) (I.to_fun x_fst)
id                └───┘                
typ               └───┘                
544             = continuous_linear_map.id,
545    { assume x_fst,
546      have : fderiv_within 𝕜 (I.to_fun ∘ I.inv_fun) (range I.to_fun) (I.to_fun x_fst)
547           = fderiv_within 𝕜 id (range I.to_fun) (I.to_fun x_fst),
id                                                           └───┘
typ                                                          └───┘
548      { refine fderiv_within_congr (I.unique_diff _ (mem_range_self _)) (λy hy, _) (by simp),
id                                                                           
typ                                                                          
549        exact model_with_corners_right_inv _ hy },
st                                                 └┘
550      rwa fderiv_within_id (I.unique_diff _ (mem_range_self _)) at this },
st                                                                         └┘
551    ext x : 1,
552    show (chart_at (H × E) p).to_fun x = (local_equiv.refl (H × E)).to_fun x,
id                                                                
typ                                                               
553    { cases x,
554      simp [chart_at, manifold.chart_at, basic_smooth_bundle_core.chart,
555            topological_fiber_bundle_core.local_triv, topological_fiber_bundle_core.local_triv',
556            basic_smooth_bundle_core.to_topological_fiber_bundle_core, tangent_bundle_core],
557      erw [local_equiv.refl_to_fun, local_equiv.refl_inv_fun, A],
558      refl },
st            └┘
559    show ∀ x, ((chart_at (H × E) p).to_local_equiv).inv_fun x = (local_equiv.refl (H × E)).inv_fun x,
id                                                                                      
typ                                                                                     
560    { rintros ⟨x_fst, x_snd⟩,
561      simp [chart_at, manifold.chart_at, basic_smooth_bundle_core.chart,
562            topological_fiber_bundle_core.local_triv, topological_fiber_bundle_core.local_triv',
563            basic_smooth_bundle_core.to_topological_fiber_bundle_core, tangent_bundle_core],
564      erw [local_equiv.refl_to_fun, local_equiv.refl_inv_fun, A],
565      refl },
st            └┘
566    show ((chart_at (H × E) p).to_local_equiv).source = (local_equiv.refl (H × E)).source,
id                                                                               
typ                                                                              
567    by simp [chart_at, manifold.chart_at, basic_smooth_bundle_core.chart,
568             topological_fiber_bundle_core.local_triv, topological_fiber_bundle_core.local_triv',
569             basic_smooth_bundle_core.to_topological_fiber_bundle_core, tangent_bundle_core,
570             local_equiv.trans_source]
571  end
st   └─┘
572  
573  variable (H)
574  /-- In the tangent bundle to the model space, the topology is the product topology, i.e., the bundle
575  is trivial -/
576  lemma tangent_bundle_model_space_topology_eq_prod :
577    tangent_bundle.topological_space I H = prod.topological_space :=
id                                        
typ                                       
578  begin
579    ext o,
580    let x : tangent_bundle I H := (I.inv_fun (0 : E), (0 : E)),
id                                                           
typ                                                          
581    let e := chart_at (H × E) x,
id                           
typ                          
582    have e_source : e.source = univ, by { simp [e], refl },
st                                                          └┘
583    have e_target : e.target = univ, by { simp [e], refl },
st                                                          └┘
584    let e' := e.to_homeomorph_of_source_eq_univ_target_eq_univ e_source e_target,
585    split,
586    { assume ho,
587      have := e'.continuous_inv_fun o ho,
588      simpa [e', tangent_bundle_model_space_chart_at] },
st                                                       └┘
589    { assume ho,
590      have := e'.continuous_to_fun o ho,
591      simpa [e', tangent_bundle_model_space_chart_at] }
st                                                       └─
592  end
st   ──┘
593  
594  end tangent_bundle